MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp3l Structured version   Visualization version   GIF version

Theorem simp3l 1088
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp3l ((𝜑𝜓 ∧ (𝜒𝜃)) → 𝜒)

Proof of Theorem simp3l
StepHypRef Expression
1 simpl 473 . 2 ((𝜒𝜃) → 𝜒)
213ad2ant3 1083 1 ((𝜑𝜓 ∧ (𝜒𝜃)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1037
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039
This theorem is referenced by:  simpl3l  1115  simpr3l  1121  simp13l  1175  simp23l  1181  simp33l  1187  tfisi  7055  tfrlem5  7473  omeulem1  7659  omeulem2  7660  uniinqs  7824  elfiun  8333  tcrank  8744  isfin2-2  9138  konigthlem  9387  gruen  9631  addid2  10216  mulcan  10661  mulcan2  10662  divass  10700  divdir  10707  div11  10710  muldivdir  10717  divcan5  10724  ltmul1  10870  ltdiv1  10884  ltmuldiv  10893  lediv2  10910  xaddass2  12077  xlt2add  12087  xmulasslem3  12113  xadddi2  12124  expaddz  12899  expmulz  12901  muldivbinom2  13042  resqrtcl  13988  o1add  14338  o1mul  14339  o1sub  14340  dvdsadd2b  15022  dvdsgcd  15255  rpexp12i  15428  pythagtriplem3  15517  pcpremul  15542  pceu  15545  pcqmul  15552  pcqdiv  15556  setsstruct  15892  f1ocpbllem  16178  funcoppc  16529  funcres  16550  catcisolem  16750  1stfcl  16831  2ndfcl  16832  prfcl  16837  evlfcl  16856  curf1cl  16862  curfcl  16866  hofcl  16893  latjlej12  17061  latmlem12  17077  latj4  17095  latj4rot  17096  symgsssg  17881  symgfisg  17882  psgnunilem4  17911  odcong  17962  cmn4  18206  ablsub4  18212  abladdsub4  18213  lsm4  18257  abvdom  18832  abvres  18833  abvtrivd  18834  lspsolvlem  19136  lbsextlem2  19153  lidlsubcl  19210  frlmbas3  20109  matmulcell  20245  marrepeval  20363  ma1repveval  20371  submaeval  20382  mdetunilem3  20414  mdetuni0  20421  mdetmul  20423  minmar1eval  20449  nllyrest  21283  hausflimlem  21777  tsmsxp  21952  psmetlecl  22114  xmetlecl  22145  prdsxmetlem  22167  ngpocelbl  22502  bndth  22751  cph2ass  23007  iscau3  23070  dvres2  23670  coemullem  24000  vieta1  24061  aalioulem4  24084  cxpcn3lem  24482  angcan  24526  dchrvmasumlema  25183  logdivsum  25216  abvcxp  25298  padicabv  25313  ax5seglem3  25805  ax5seglem6  25808  axpasch  25815  axeuclid  25837  axcontlem4  25841  axcontlem8  25845  wlkl1loop  26528  trlsonwlkon  26600  pthontrlon  26637  wspthsswwlknon  26811  frgr2wwlkeqm  27182  adjlnop  28929  xreceu  29615  orngmul  29788  rhmdvd  29806  measvunilem  30260  measvunilem0  30261  measres  30270  bnj1128  31043  subdivcomb1  31597  subdivcomb2  31598  nosupbnd1lem4  31841  nosupbnd1lem5  31842  cgrcomim  32080  cgrcoml  32087  cgrcomr  32088  cgrdegen  32095  segconeu  32102  btwnintr  32110  btwnexch3  32111  btwnouttr2  32113  btwnouttr  32115  btwnexch  32116  trisegint  32119  lineext  32167  linecgr  32172  lineid  32174  idinside  32175  btwnconn1lem3  32180  btwnconn1lem4  32181  btwnconn1lem7  32184  btwnconn1lem14  32191  btwnconn2  32193  midofsegid  32195  btwnoutside  32216  outsideoftr  32220  lineunray  32238  lineelsb2  32239  cnres2  33542  heibor  33600  lsmcv2  34142  lcvat  34143  lcvexchlem4  34150  lcvexchlem5  34151  lfladd  34179  lflsub  34180  lflmul  34181  lshpkrlem4  34226  latm4  34346  omlmod1i2N  34373  cvlatexch3  34451  cvlsupr7  34461  hlatj4  34486  hlrelat3  34524  cvrval3  34525  atcvrj1  34543  atlelt  34550  2atlt  34551  2atjm  34557  3noncolr2  34561  athgt  34568  3dimlem2  34571  3dimlem4  34576  3dimlem4OLDN  34577  3dim3  34581  1cvratex  34585  ps-1  34589  ps-2  34590  hlatexch3N  34592  llnle  34630  atcvrlln2  34631  atcvrlln  34632  lplni2  34649  lplnle  34652  lplnnle2at  34653  llncvrlpln2  34669  lplnexllnN  34676  2llnmeqat  34683  lvolnle3at  34694  4atlem0ae  34706  lplncvrlvol2  34727  lnjatN  34892  lncvrat  34894  cdlemblem  34905  elpaddri  34914  paddasslem2  34933  paddasslem16  34947  padd4N  34952  hlmod1i  34968  dalawlem2  34984  pclfinN  35012  pexmidlem4N  35085  pl42lem1N  35091  lhp2lt  35113  lhpexle1  35120  lhpexle2lem  35121  lhpj1  35134  lhpmcvr5N  35139  lhp2at0  35144  lhp2atnle  35145  lhp2at0nle  35147  lhple  35154  lhpat  35155  lhpat4N  35156  4atexlempnq  35167  4atexlem7  35187  4atex  35188  ltrn11  35238  ltrnle  35241  ltrnm  35243  ltrnj  35244  ltrncvr  35245  ltrnel  35251  ltrncnvel  35254  ltrncnv  35258  ltrnmwOLD  35264  trlval2  35276  trlcnv  35278  trljat1  35279  trljat2  35280  trlat  35282  trl0  35283  trlnidat  35286  trlnid  35292  cdlemc1  35304  cdlemc2  35305  cdlemc5  35308  cdlemd2  35312  cdlemd7  35317  cdlemd8  35318  cdlemd9  35319  cdleme0e  35330  cdleme3g  35347  cdleme3h  35348  cdleme3  35350  cdleme5  35353  cdleme10  35367  cdleme11a  35373  cdleme11c  35374  cdleme11h  35379  cdleme11j  35380  cdleme0nex  35403  cdleme18a  35404  cdleme18b  35405  cdleme22gb  35407  cdleme20zN  35414  cdleme20yOLD  35416  cdleme20c  35425  cdleme20k  35433  cdleme21a  35439  cdleme21b  35440  cdleme21c  35441  cdleme21h  35448  cdleme22b  35455  cdleme22d  35457  cdleme22f  35460  cdleme25a  35467  cdleme25c  35469  cdleme25dN  35470  cdleme26ee  35474  cdleme30a  35492  cdlemefr29bpre0N  35520  cdlemefr29clN  35521  cdlemefr32fvaN  35523  cdlemefr32fva1  35524  cdlemefs29bpre0N  35530  cdlemefs29bpre1N  35531  cdlemefs29cpre1N  35532  cdlemefs29clN  35533  cdleme43fsv1snlem  35534  cdlemefs32fvaN  35536  cdlemefs32fva1  35537  cdlemefs31fv1  35538  cdleme36a  35574  cdleme39a  35579  cdleme42a  35585  cdleme42c  35586  cdleme17d3  35610  cdleme48fv  35613  cdleme48bw  35616  cdleme48b  35617  cdlemeg46rgv  35642  cdlemeg46req  35643  cdlemeg46gfv  35644  cdleme48d  35649  cdleme50trn2a  35664  cdleme50trn2  35665  cdleme50ltrn  35671  cdlemf1  35675  cdlemf  35677  trlord  35683  cdlemg2dN  35704  cdlemg2fvlem  35708  cdlemg2l  35717  cdlemg7fvbwN  35721  cdlemg7aN  35739  cdlemg10bALTN  35750  cdlemg10c  35753  cdlemg17a  35775  cdlemg17dALTN  35778  cdlemg31b0a  35809  cdlemg31a  35811  cdlemg31b  35812  cdlemg34  35826  cdlemg36  35828  ltrnco  35833  trlcoabs2N  35836  trlcolem  35840  cdlemg48  35851  tgrpov  35862  tendoco2  35882  tendoplco2  35893  cdlemh1  35929  cdlemi1  35932  cdlemi2  35933  cdlemj3  35937  tendoid0  35939  cdlemk1  35945  cdlemk2  35946  cdlemk4  35948  cdlemk8  35952  cdlemk9  35953  cdlemk9bN  35954  cdlemk10  35957  cdlemk26b-3  36019  cdlemk26-3  36020  cdlemk28-3  36022  cdlemk37  36028  cdlemk39  36030  cdlemkfid1N  36035  cdlemkid1  36036  cdlemky  36040  cdlemkyu  36041  cdlemk19ylem  36044  cdlemk19xlem  36056  cdlemk11t  36060  cdlemk51  36067  cdlemkyyN  36076  cdleml6  36095  cdleml7  36096  cdleml8  36097  cdleml9  36098  erngdvlem4  36105  erngdvlem4-rN  36113  tendospcanN  36138  dia11N  36163  cdlemm10N  36233  dib11N  36275  dicvaddcl  36305  dicvscacl  36306  cdlemn6  36317  dihvalcq2  36362  dihopelvalcpre  36363  dihord6b  36375  dihord5apre  36377  dihmeetlem1N  36405  dihmeetlem2N  36414  dihglbcpreN  36415  dihjatc1  36426  dihmeetlem20N  36441  dih1dimatlem0  36443  dihatlat  36449  dihglblem6  36455  dochexmidlem4  36578  mapdpglem32  36820  mapdh8ad  36894  mapdh9aOLDN  36906  hdmap11lem2  36960  hdmap14lem6  36991  mzpsubst  37137  pellex  37225  pellfundex  37276  pellfund14gap  37277  qirropth  37299  rmxypos  37340  congmul  37360  congsub  37363  mzpcong  37365  coprmdvdsb  37378  jm2.15nn0  37396  jm2.16nn0  37397  rpnnen3lem  37424  idomsubgmo  37602  relexp01min  37831  mullimc  39654  islptre  39657  limccog  39658  mullimcf  39661  addlimc  39686  0ellimcdiv  39687  limsupre3lem  39770  stoweidlem57  40043  fourierdlem48  40140  fourierdlem80  40172  fourierdlem113  40205  ovncvrrp  40547  opnvonmbllem2  40616  ovolval5lem3  40637  ovnovollem3  40641
  Copyright terms: Public domain W3C validator