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

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

Proof of Theorem simp3l
StepHypRef Expression
1 simpl 472 . 2 ((𝜒𝜃) → 𝜒)
213ad2ant3 1104 1 ((𝜑𝜓 ∧ (𝜒𝜃)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 385  df-3an 1056
This theorem is referenced by:  simpl3l  1136  simpr3l  1142  simp13l  1196  simp23l  1202  simp33l  1208  tfisi  7100  tfrlem5  7521  omeulem1  7707  omeulem2  7708  uniinqs  7870  elfiun  8377  tcrank  8785  isfin2-2  9179  konigthlem  9428  gruen  9672  addid2  10257  mulcan  10702  mulcan2  10703  divass  10741  divdir  10748  div11  10751  muldivdir  10758  divcan5  10765  ltmul1  10911  ltdiv1  10925  ltmuldiv  10934  lediv2  10951  xaddass2  12118  xlt2add  12128  xmulasslem3  12154  xadddi2  12165  expaddz  12944  expmulz  12946  muldivbinom2  13087  resqrtcl  14038  o1add  14388  o1mul  14389  o1sub  14390  dvdsadd2b  15075  dvdsgcd  15308  rpexp12i  15481  pythagtriplem3  15570  pcpremul  15595  pceu  15598  pcqmul  15605  pcqdiv  15609  setsstruct  15945  f1ocpbllem  16231  funcoppc  16582  funcres  16603  catcisolem  16803  1stfcl  16884  2ndfcl  16885  prfcl  16890  evlfcl  16909  curf1cl  16915  curfcl  16919  hofcl  16946  latjlej12  17114  latmlem12  17130  latj4  17148  latj4rot  17149  symgsssg  17933  symgfisg  17934  psgnunilem4  17963  odcong  18014  cmn4  18258  ablsub4  18264  abladdsub4  18265  lsm4  18309  abvdom  18886  abvres  18887  abvtrivd  18888  lspsolvlem  19190  lbsextlem2  19207  lidlsubcl  19264  frlmbas3  20163  matmulcell  20299  marrepeval  20417  ma1repveval  20425  submaeval  20436  mdetunilem3  20468  mdetuni0  20475  mdetmul  20477  minmar1eval  20503  nllyrest  21337  hausflimlem  21830  tsmsxp  22005  psmetlecl  22167  xmetlecl  22198  prdsxmetlem  22220  ngpocelbl  22555  bndth  22804  cph2ass  23059  iscau3  23122  dvres2  23721  coemullem  24051  vieta1  24112  aalioulem4  24135  cxpcn3lem  24533  angcan  24577  dchrvmasumlema  25234  logdivsum  25267  abvcxp  25349  padicabv  25364  ax5seglem3  25856  ax5seglem6  25859  axpasch  25866  axeuclid  25888  axcontlem4  25892  axcontlem8  25896  wlkl1loop  26590  trlsonwlkon  26662  pthontrlon  26699  wspthsswwlknon  26886  frgr2wwlkeqm  27311  adjlnop  29073  xreceu  29758  orngmul  29931  rhmdvd  29949  measvunilem  30403  measvunilem0  30404  measres  30413  bnj1128  31184  subdivcomb1  31737  subdivcomb2  31738  nosupbnd1lem4  31982  nosupbnd1lem5  31983  cgrcomim  32221  cgrcoml  32228  cgrcomr  32229  cgrdegen  32236  segconeu  32243  btwnintr  32251  btwnexch3  32252  btwnouttr2  32254  btwnouttr  32256  btwnexch  32257  trisegint  32260  lineext  32308  linecgr  32313  lineid  32315  idinside  32316  btwnconn1lem3  32321  btwnconn1lem4  32322  btwnconn1lem7  32325  btwnconn1lem14  32332  btwnconn2  32334  midofsegid  32336  btwnoutside  32357  outsideoftr  32361  lineunray  32379  lineelsb2  32380  cnres2  33692  heibor  33750  lsmcv2  34634  lcvat  34635  lcvexchlem4  34642  lcvexchlem5  34643  lfladd  34671  lflsub  34672  lflmul  34673  lshpkrlem4  34718  latm4  34838  omlmod1i2N  34865  cvlatexch3  34943  cvlsupr7  34953  hlatj4  34978  hlrelat3  35016  cvrval3  35017  atcvrj1  35035  atlelt  35042  2atlt  35043  2atjm  35049  3noncolr2  35053  athgt  35060  3dimlem2  35063  3dimlem4  35068  3dimlem4OLDN  35069  3dim3  35073  1cvratex  35077  ps-1  35081  ps-2  35082  hlatexch3N  35084  llnle  35122  atcvrlln2  35123  atcvrlln  35124  lplni2  35141  lplnle  35144  lplnnle2at  35145  llncvrlpln2  35161  lplnexllnN  35168  2llnmeqat  35175  lvolnle3at  35186  4atlem0ae  35198  lplncvrlvol2  35219  lnjatN  35384  lncvrat  35386  cdlemblem  35397  elpaddri  35406  paddasslem2  35425  paddasslem16  35439  padd4N  35444  hlmod1i  35460  dalawlem2  35476  pclfinN  35504  pexmidlem4N  35577  pl42lem1N  35583  lhp2lt  35605  lhpexle1  35612  lhpexle2lem  35613  lhpj1  35626  lhpmcvr5N  35631  lhp2at0  35636  lhp2atnle  35637  lhp2at0nle  35639  lhple  35646  lhpat  35647  lhpat4N  35648  4atexlempnq  35659  4atexlem7  35679  4atex  35680  ltrn11  35730  ltrnle  35733  ltrnm  35735  ltrnj  35736  ltrncvr  35737  ltrnel  35743  ltrncnvel  35746  ltrncnv  35750  ltrnmwOLD  35756  trlval2  35768  trlcnv  35770  trljat1  35771  trljat2  35772  trlat  35774  trl0  35775  trlnidat  35778  trlnid  35784  cdlemc1  35796  cdlemc2  35797  cdlemc5  35800  cdlemd2  35804  cdlemd7  35809  cdlemd8  35810  cdlemd9  35811  cdleme0e  35822  cdleme3g  35839  cdleme3h  35840  cdleme3  35842  cdleme5  35845  cdleme10  35859  cdleme11a  35865  cdleme11c  35866  cdleme11h  35871  cdleme11j  35872  cdleme0nex  35895  cdleme18a  35896  cdleme18b  35897  cdleme22gb  35899  cdleme20zN  35906  cdleme20c  35916  cdleme20k  35924  cdleme21a  35930  cdleme21b  35931  cdleme21c  35932  cdleme21h  35939  cdleme22b  35946  cdleme22d  35948  cdleme22f  35951  cdleme25a  35958  cdleme25c  35960  cdleme25dN  35961  cdleme26ee  35965  cdleme30a  35983  cdlemefr29bpre0N  36011  cdlemefr29clN  36012  cdlemefr32fvaN  36014  cdlemefr32fva1  36015  cdlemefs29bpre0N  36021  cdlemefs29bpre1N  36022  cdlemefs29cpre1N  36023  cdlemefs29clN  36024  cdleme43fsv1snlem  36025  cdlemefs32fvaN  36027  cdlemefs32fva1  36028  cdlemefs31fv1  36029  cdleme36a  36065  cdleme39a  36070  cdleme42a  36076  cdleme42c  36077  cdleme17d3  36101  cdleme48fv  36104  cdleme48bw  36107  cdleme48b  36108  cdlemeg46rgv  36133  cdlemeg46req  36134  cdlemeg46gfv  36135  cdleme48d  36140  cdleme50trn2a  36155  cdleme50trn2  36156  cdleme50ltrn  36162  cdlemf1  36166  cdlemf  36168  trlord  36174  cdlemg2dN  36195  cdlemg2fvlem  36199  cdlemg2l  36208  cdlemg7fvbwN  36212  cdlemg7aN  36230  cdlemg10bALTN  36241  cdlemg10c  36244  cdlemg17a  36266  cdlemg17dALTN  36269  cdlemg31b0a  36300  cdlemg31a  36302  cdlemg31b  36303  cdlemg34  36317  cdlemg36  36319  ltrnco  36324  trlcoabs2N  36327  trlcolem  36331  cdlemg48  36342  tgrpov  36353  tendoco2  36373  tendoplco2  36384  cdlemh1  36420  cdlemi1  36423  cdlemi2  36424  cdlemj3  36428  tendoid0  36430  cdlemk1  36436  cdlemk2  36437  cdlemk4  36439  cdlemk8  36443  cdlemk9  36444  cdlemk9bN  36445  cdlemk10  36448  cdlemk26b-3  36510  cdlemk26-3  36511  cdlemk28-3  36513  cdlemk37  36519  cdlemk39  36521  cdlemkfid1N  36526  cdlemkid1  36527  cdlemky  36531  cdlemkyu  36532  cdlemk19ylem  36535  cdlemk19xlem  36547  cdlemk11t  36551  cdlemk51  36558  cdlemkyyN  36567  cdleml6  36586  cdleml7  36587  cdleml8  36588  cdleml9  36589  erngdvlem4  36596  erngdvlem4-rN  36604  tendospcanN  36629  dia11N  36654  cdlemm10N  36724  dib11N  36766  dicvaddcl  36796  dicvscacl  36797  cdlemn6  36808  dihvalcq2  36853  dihopelvalcpre  36854  dihord6b  36866  dihord5apre  36868  dihmeetlem1N  36896  dihmeetlem2N  36905  dihglbcpreN  36906  dihjatc1  36917  dihmeetlem20N  36932  dih1dimatlem0  36934  dihatlat  36940  dihglblem6  36946  dochexmidlem4  37069  mapdpglem32  37311  mapdh8ad  37385  mapdh9aOLDN  37397  hdmap11lem2  37451  hdmap14lem6  37482  mzpsubst  37628  pellex  37716  pellfundex  37767  pellfund14gap  37768  qirropth  37790  rmxypos  37831  congmul  37851  congsub  37854  mzpcong  37856  coprmdvdsb  37869  jm2.15nn0  37887  jm2.16nn0  37888  rpnnen3lem  37915  idomsubgmo  38093  relexp01min  38322  mullimc  40166  islptre  40169  limccog  40170  mullimcf  40173  addlimc  40198  0ellimcdiv  40199  limsupre3lem  40282  stoweidlem57  40592  fourierdlem48  40689  fourierdlem80  40721  fourierdlem113  40754  ovncvrrp  41099  opnvonmbllem2  41168  ovolval5lem3  41189  ovnovollem3  41193
  Copyright terms: Public domain W3C validator