Theorem simprr 415

Description: Simplification of a conjunction.

Assertion

Ref	Expression
simprr	⊢ ((φ ⋀ (ψ ⋀ χ)) → χ)

Proof of Theorem simprr

Step	Hyp	Ref	Expression
1		id 59	. 2 ⊢ (χ → χ)
2	1	ad2antll 407	1 ⊢ ((φ ⋀ (ψ ⋀ χ)) → χ)

Syntax hints:   → wi 3   ⋀ wa 221

This theorem is referenced by:  reuuniss2 3114  1stconst 4190  2ndconst 4191  sdomdomtr 4614  mulgt0sr 5368  cnegexlem1 5499  muladd 5575  divass 5887  lemul2aOLD 5984  ltmul12a 5985  lemul12a 5988  lemulge11 5992  lt2mul2div 6016  lediv12a 6041  modadd1 6477  modmul1 6478  elfzle2 6612  elfz2nn0 6625  fzrev 6642  exprecOLD 6790  le2sq2 6829  bernneq 6849  bernneqOLD 6850  fsumdivc 7238  fsumdivcALT 7239  fsum0diaglem2 7462  acdc2lem2 7701  acdc5lem2 7704  tgval3 7837  tgss2 7849  ssnei2 7940  cnpcl 7974  cnco 7978  cncnplem1 7984  cnconst 7990  blcntr 8055  blelrn 8058  blss 8063  opnuni 8078  metcnplem 8097  lmle 8171  xplmi 8184  lmcau 8207  cmsss 8208  bcthlem11 8220  grpidinvlem2 8262  grpinvid1 8289  grpinvid2 8290  grplcan 8292  abl4 8346  ringideu 8387  nvsubadd 8522  nvnpcan 8527  nvmeq0 8531  nvabs 8548  vacnlem6 8587  lnomul 8675  ubthlem3 8789  psasym 8913  5oalem5 9881  unoplin 10124  hmoplin 10146  bralnfn 10152  hmops 10224  hmopm 10225  hmopco 10227  adjadd 10305  kbass3 10331  strlem3a 10460  csmdsymi 10542  ghomf1olem 10681  cljo 10834  clme 10835  definc 10869  domncnt 10872  ranncnt 10873  toplat 10884  ismnd1 10927  rnplrnml 10948  hmeobc 11048  altretop 11144  trnij 11160  imonclem 11268  idmon 11272  codsubc 11307  xpss1 11403  finminlem 11418  elfiun 11421  finsschain 11425  ordiso 11426  hartoglem 11435  omsublim 11448  omsubinit 11451  cnntr 11474  subntr 11482  cnsubsp2 11484  compsub 11488  uncomp 11490  compfipin0lem 11492  compfipin0 11493  alexsublem2 11497  subtopmetlem 11505  subtopmet 11506  reconnlem5 11511  ivthALT 11515  2ndcsb 11537  2ndc1stc 11538  2ndcctbss 11539  isfne3 11543  fneint 11547  fnetr 11556  topfneec 11562  fnessref 11564  lfinpfin 11574  comppfsc 11578  neibastop2lem1 11580  neibastop2lem2 11581  fnemeet2 11590  fnejoin1 11591  fbunfip 11631  isufil2 11650  filssufillem 11655  ufileu 11658  filufint 11659  ufinffr 11663  ufilen 11664  limfilcf 11683  cnpfillim 11686  elfilmap 11690  elfilmap2 11691  elfilmap3 11692  rnelfm 11699  fmfnfmlem1 11700  fmfnfmlem2 11701  fmfnfmlem4 11703  flimfbas 11713  fcluscf 11724  flimfnfcls 11727  fcluscnp 11730  fcluscomplem 11732  tosdir 11755  filnetlem4 11766  filnetlem5 11767  filnet 11768  ssga 11777  gapmlem 11783  oprabopabf 11807  fipreima 11848  metsstop 11909  cnres 11950  2txcn 11982  txsubsp 11983  sstotbnd 11992  totbndbnd 12000  ismtyhmeolem 12006  heiborlem18 12028  rrntotbndlem2 12077  rrntotbnd 12078  phtpyco 12098  phtpcer 12104

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 145  df-an 223

Copyright terms: Public domain