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

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

Proof of Theorem simp3l
StepHypRef Expression
1 simpl 470 . 2 ((𝜒𝜃) → 𝜒)
213ad2ant3 1158 1 ((𝜑𝜓 ∧ (𝜒𝜃)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  simpl3lOLD  1295  simpr3lOLD  1307  simp13l  1380  simp23l  1386  simp33l  1392  tfisi  7282  tfrlem5  7706  omeulem1  7893  omeulem2  7894  uniinqs  8056  elfiun  8569  tcrank  8988  isfin2-2  9420  konigthlem  9669  gruen  9913  addid2  10498  mulcan  10943  mulcan2  10944  divass  10982  divdir  10989  div11  10992  muldivdir  10999  divcan5  11006  ltmul1  11152  ltdiv1  11166  ltmuldiv  11175  lediv2  11192  xaddass2  12292  xlt2add  12302  xmulasslem3  12328  xadddi2  12339  expaddz  13121  expmulz  13123  muldivbinom2  13264  resqrtcl  14211  o1add  14561  o1mul  14562  o1sub  14563  dvdsadd2b  15245  dvdsgcd  15474  rpexp12i  15645  pythagtriplem3  15734  pcpremul  15759  pceu  15762  pcqmul  15769  pcqdiv  15773  setsstruct  16103  f1ocpbllem  16383  funcoppc  16733  funcres  16754  catcisolem  16954  1stfcl  17036  2ndfcl  17037  prfcl  17042  evlfcl  17061  curf1cl  17067  curfcl  17071  hofcl  17098  latjlej12  17266  latmlem12  17282  latj4  17300  latj4rot  17301  symgsssg  18082  symgfisg  18083  psgnunilem4  18112  odcong  18163  cmn4  18407  ablsub4  18413  abladdsub4  18414  lsm4  18458  abvdom  19036  abvres  19037  abvtrivd  19038  lspsolvlem  19344  lbsextlem2  19362  lidlsubcl  19419  frlmbas3  20319  matmulcell  20455  matmulcellOLD  20456  marrepeval  20574  ma1repveval  20582  submaeval  20593  mdetunilem3  20625  mdetuni0  20632  mdetmul  20634  minmar1eval  20660  nllyrest  21497  hausflimlem  21990  tsmsxp  22165  psmetlecl  22327  xmetlecl  22358  prdsxmetlem  22380  ngpocelbl  22715  bndth  22964  cph2ass  23219  iscau3  23282  dvres2  23884  coemullem  24214  vieta1  24275  aalioulem4  24298  cxpcn3lem  24696  angcan  24740  dchrvmasumlema  25397  logdivsum  25430  abvcxp  25512  padicabv  25527  ax5seglem3  26019  ax5seglem6  26022  axpasch  26029  axeuclid  26051  axcontlem4  26055  axcontlem8  26059  wlkl1loop  26756  trlsonwlkon  26828  pthontrlon  26865  wspthsswwlknon  27055  frgr2wwlkeqm  27500  adjlnop  29267  xreceu  29949  orngmul  30122  rhmdvd  30140  measvunilem  30594  measvunilem0  30595  measres  30604  bnj1128  31375  subdivcomb1  31927  subdivcomb2  31928  nosupbnd1lem4  32172  nosupbnd1lem5  32173  cgrcomim  32411  cgrcoml  32418  cgrcomr  32419  cgrdegen  32426  segconeu  32433  btwnintr  32441  btwnexch3  32442  btwnouttr2  32444  btwnouttr  32446  btwnexch  32447  trisegint  32450  lineext  32498  linecgr  32503  lineid  32505  idinside  32506  btwnconn1lem3  32511  btwnconn1lem4  32512  btwnconn1lem7  32515  btwnconn1lem14  32522  btwnconn2  32524  midofsegid  32526  btwnoutside  32547  outsideoftr  32551  lineunray  32569  lineelsb2  32570  cnres2  33867  heibor  33925  lsmcv2  34803  lcvat  34804  lcvexchlem4  34811  lcvexchlem5  34812  lfladd  34840  lflsub  34841  lflmul  34842  lshpkrlem4  34887  latm4  35007  omlmod1i2N  35034  cvlatexch3  35112  cvlsupr7  35122  hlatj4  35148  hlrelat3  35186  cvrval3  35187  atcvrj1  35205  atlelt  35212  2atlt  35213  2atjm  35219  3noncolr2  35223  athgt  35230  3dimlem2  35233  3dimlem4  35238  3dimlem4OLDN  35239  3dim3  35243  1cvratex  35247  ps-1  35251  ps-2  35252  hlatexch3N  35254  llnle  35292  atcvrlln2  35293  atcvrlln  35294  lplni2  35311  lplnle  35314  lplnnle2at  35315  llncvrlpln2  35331  lplnexllnN  35338  2llnmeqat  35345  lvolnle3at  35356  4atlem0ae  35368  lplncvrlvol2  35389  lnjatN  35554  lncvrat  35556  cdlemblem  35567  elpaddri  35576  paddasslem2  35595  paddasslem16  35609  padd4N  35614  hlmod1i  35630  dalawlem2  35646  pclfinN  35674  pexmidlem4N  35747  pl42lem1N  35753  lhp2lt  35775  lhpexle1  35782  lhpexle2lem  35783  lhpj1  35796  lhpmcvr5N  35801  lhp2at0  35806  lhp2atnle  35807  lhp2at0nle  35809  lhple  35816  lhpat  35817  lhpat4N  35818  4atexlempnq  35829  4atexlem7  35849  4atex  35850  ltrn11  35900  ltrnle  35903  ltrnm  35905  ltrnj  35906  ltrncvr  35907  ltrnel  35913  ltrncnvel  35916  ltrncnv  35920  ltrnmwOLD  35926  trlval2  35938  trlcnv  35940  trljat1  35941  trljat2  35942  trlat  35944  trl0  35945  trlnidat  35948  trlnid  35954  cdlemc1  35966  cdlemc2  35967  cdlemc5  35970  cdlemd2  35974  cdlemd7  35979  cdlemd8  35980  cdlemd9  35981  cdleme0e  35992  cdleme3g  36009  cdleme3h  36010  cdleme3  36012  cdleme5  36015  cdleme10  36029  cdleme11a  36035  cdleme11c  36036  cdleme11h  36041  cdleme11j  36042  cdleme0nex  36065  cdleme18a  36066  cdleme18b  36067  cdleme22gb  36069  cdleme20zN  36076  cdleme20c  36086  cdleme20k  36094  cdleme21a  36100  cdleme21b  36101  cdleme21c  36102  cdleme21h  36109  cdleme22b  36116  cdleme22d  36118  cdleme22f  36121  cdleme25a  36128  cdleme25c  36130  cdleme25dN  36131  cdleme26ee  36135  cdleme30a  36153  cdlemefr29bpre0N  36181  cdlemefr29clN  36182  cdlemefr32fvaN  36184  cdlemefr32fva1  36185  cdlemefs29bpre0N  36191  cdlemefs29bpre1N  36192  cdlemefs29cpre1N  36193  cdlemefs29clN  36194  cdleme43fsv1snlem  36195  cdlemefs32fvaN  36197  cdlemefs32fva1  36198  cdlemefs31fv1  36199  cdleme36a  36235  cdleme39a  36240  cdleme42a  36246  cdleme42c  36247  cdleme17d3  36271  cdleme48fv  36274  cdleme48bw  36277  cdleme48b  36278  cdlemeg46rgv  36303  cdlemeg46req  36304  cdlemeg46gfv  36305  cdleme48d  36310  cdleme50trn2a  36325  cdleme50trn2  36326  cdleme50ltrn  36332  cdlemf1  36336  cdlemf  36338  trlord  36344  cdlemg2dN  36365  cdlemg2fvlem  36369  cdlemg2l  36378  cdlemg7fvbwN  36382  cdlemg7aN  36400  cdlemg10bALTN  36411  cdlemg10c  36414  cdlemg17a  36436  cdlemg17dALTN  36439  cdlemg31b0a  36470  cdlemg31a  36472  cdlemg31b  36473  cdlemg34  36487  cdlemg36  36489  ltrnco  36494  trlcoabs2N  36497  trlcolem  36501  cdlemg48  36512  tgrpov  36523  tendoco2  36543  tendoplco2  36554  cdlemh1  36590  cdlemi1  36593  cdlemi2  36594  cdlemj3  36598  tendoid0  36600  cdlemk1  36606  cdlemk2  36607  cdlemk4  36609  cdlemk8  36613  cdlemk9  36614  cdlemk9bN  36615  cdlemk10  36618  cdlemk26b-3  36680  cdlemk26-3  36681  cdlemk28-3  36683  cdlemk37  36689  cdlemk39  36691  cdlemkfid1N  36696  cdlemkid1  36697  cdlemky  36701  cdlemkyu  36702  cdlemk19ylem  36705  cdlemk19xlem  36717  cdlemk11t  36721  cdlemk51  36728  cdlemkyyN  36737  cdleml6  36756  cdleml7  36757  cdleml8  36758  cdleml9  36759  erngdvlem4  36766  erngdvlem4-rN  36774  tendospcanN  36798  dia11N  36823  cdlemm10N  36893  dib11N  36935  dicvaddcl  36965  dicvscacl  36966  cdlemn6  36977  dihvalcq2  37022  dihopelvalcpre  37023  dihord6b  37035  dihord5apre  37037  dihmeetlem1N  37065  dihmeetlem2N  37074  dihglbcpreN  37075  dihjatc1  37086  dihmeetlem20N  37101  dih1dimatlem0  37103  dihatlat  37109  dihglblem6  37115  dochexmidlem4  37238  mapdpglem32  37480  mapdh8ad  37554  mapdh9aOLDN  37565  hdmap11lem2  37617  hdmap14lem6  37648  mzpsubst  37807  pellex  37895  pellfundex  37946  pellfund14gap  37947  qirropth  37968  rmxypos  38009  congmul  38029  congsub  38032  mzpcong  38034  coprmdvdsb  38047  jm2.15nn0  38065  jm2.16nn0  38066  rpnnen3lem  38093  idomsubgmo  38271  relexp01min  38499  mullimc  40322  islptre  40325  limccog  40326  mullimcf  40329  addlimc  40354  0ellimcdiv  40355  limsupre3lem  40438  stoweidlem57  40747  fourierdlem48  40844  fourierdlem80  40876  fourierdlem113  40909  ovncvrrp  41254  opnvonmbllem2  41323  ovolval5lem3  41344  ovnovollem3  41348
  Copyright terms: Public domain W3C validator