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

Theorem simp3l 983
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp3l  |-  ( (
ph  /\  ps  /\  ( ch  /\  th ) )  ->  ch )

Proof of Theorem simp3l
StepHypRef Expression
1 simpl 443 . 2  |-  ( ( ch  /\  th )  ->  ch )
213ad2ant3 978 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  simpl3l  1010  simpr3l  1016  simp13l  1070  simp23l  1076  simp33l  1082  disjss3  4022  tfisi  4649  omeulem1  6580  omeulem2  6581  elfiun  7183  tcrank  7554  isfin2-2  7945  konigthlem  8190  gruen  8434  addid2  8995  mulcan  9405  mulcan2  9406  divass  9442  divdir  9447  div11  9450  divcan5  9462  ltmul1  9606  ltdiv1  9620  ltmuldiv  9626  lediv2  9646  xaddass2  10570  xlt2add  10580  xmulasslem3  10606  xadddi2  10617  expaddz  11146  expmulz  11148  resqrcl  11739  o1add  12087  o1mul  12088  o1sub  12089  dvdsadd2b  12571  dvdsgcd  12722  rpexp12i  12801  pythagtriplem3  12871  pcpremul  12896  pceu  12899  pcqmul  12906  pcqdiv  12910  f1ocpbllem  13426  funcoppc  13749  funcres  13770  catcisolem  13938  1stfcl  13971  2ndfcl  13972  prfcl  13977  evlfcl  13996  curf1cl  14002  curfcl  14006  hofcl  14033  latjlej12  14173  latmlem12  14189  latj4  14207  latj4rot  14208  odcong  14864  cmn4  15108  ablsub4  15114  abladdsub4  15115  lsm4  15152  abvdom  15603  abvres  15604  abvtrivd  15605  lspsolvlem  15895  lbsextlem2  15912  nllyrest  17212  hausflimlem  17674  tsmsxp  17837  xmetlecl  17911  prdsxmetlem  17932  bndth  18456  cph2ass  18648  iscau3  18704  dvres2  19262  coemullem  19631  vieta1  19692  aalioulem4  19715  cxpcn3lem  20087  angcan  20100  dchrvmasumlema  20649  logdivsum  20682  abvcxp  20764  padicabv  20779  gxneg  20933  gxsuc  20939  gxmodid  20946  adjlnop  22666  xreceu  23105  measvunilem  23540  measvunilem0  23541  subdivcomb1  24090  subdivcomb2  24091  ax5seglem3  24559  ax5seglem6  24562  axpasch  24569  axeuclid  24591  axcontlem4  24595  axcontlem8  24599  cgrcomim  24612  cgrcoml  24619  cgrcomr  24620  cgrdegen  24627  segconeu  24634  btwnintr  24642  btwnexch3  24643  btwnouttr2  24645  btwnouttr  24647  btwnexch  24648  trisegint  24651  lineext  24699  linecgr  24704  lineid  24706  idinside  24707  btwnconn1lem3  24712  btwnconn1lem4  24713  btwnconn1lem7  24716  btwnconn1lem14  24723  btwnconn2  24725  midofsegid  24727  btwnoutside  24748  outsideoftr  24752  lineunray  24770  lineelsb2  24771  uninqs  25039  infxpg  25095  prltub  25260  mulinvsca  25480  truni3  25507  prdnei  25573  supnufb  25630  mulmulvec  25687  distsava  25689  vtarl  25887  cmpmorass  25966  cnres2  26483  heibor  26545  mzpsubst  26826  pellex  26920  pellfundex  26971  pellfund14gap  26972  qirropth  26993  rmxypos  27034  congmul  27054  congsub  27057  mzpcong  27059  coprmdvdsb  27074  jm2.15nn0  27096  jm2.16nn0  27097  rpnnen3lem  27124  symgsssg  27408  symgfisg  27409  psgnunilem4  27420  idomsubgmo  27514  stoweidlem57  27806  bnj1128  29020  lsmcv2  29219  lcvat  29220  lcvexchlem4  29227  lcvexchlem5  29228  lfladd  29256  lflsub  29257  lflmul  29258  lshpkrlem4  29303  latm4  29423  omlmod1i2N  29450  cvlatexch3  29528  cvlsupr7  29538  hlatj4  29563  hlrelat3  29601  cvrval3  29602  atcvrj1  29620  atlelt  29627  2atlt  29628  2atjm  29634  3noncolr2  29638  athgt  29645  3dimlem2  29648  3dimlem4  29653  3dimlem4OLDN  29654  3dim3  29658  1cvratex  29662  ps-1  29666  ps-2  29667  hlatexch3N  29669  llnle  29707  atcvrlln2  29708  atcvrlln  29709  lplni2  29726  lplnle  29729  lplnnle2at  29730  llncvrlpln2  29746  lplnexllnN  29753  2llnmeqat  29760  lvolnle3at  29771  4atlem0ae  29783  lplncvrlvol2  29804  lnjatN  29969  lncvrat  29971  cdlemblem  29982  elpaddri  29991  paddasslem2  30010  paddasslem16  30024  padd4N  30029  hlmod1i  30045  dalawlem2  30061  pclfinN  30089  pexmidlem4N  30162  pl42lem1N  30168  lhp2lt  30190  lhpexle1  30197  lhpexle2lem  30198  lhpj1  30211  lhpmcvr5N  30216  lhp2at0  30221  lhp2atnle  30222  lhp2at0nle  30224  lhple  30231  lhpat  30232  lhpat4N  30233  4atexlempnq  30244  4atexlem7  30264  4atex  30265  ltrn11  30315  ltrnle  30318  ltrnm  30320  ltrnj  30321  ltrncvr  30322  ltrnel  30328  ltrncnvel  30331  ltrncnv  30335  ltrnmw  30340  trlval2  30352  trlcnv  30354  trljat1  30355  trljat2  30356  trlat  30358  trl0  30359  trlnidat  30362  trlnid  30368  cdlemc1  30380  cdlemc2  30381  cdlemc5  30384  cdlemd2  30388  cdlemd7  30393  cdlemd8  30394  cdlemd9  30395  cdleme0e  30406  cdleme3g  30423  cdleme3h  30424  cdleme3  30426  cdleme5  30429  cdleme10  30443  cdleme11a  30449  cdleme11c  30450  cdleme11h  30455  cdleme11j  30456  cdleme0nex  30479  cdleme18a  30480  cdleme18b  30481  cdleme22gb  30483  cdleme20zN  30490  cdleme20y  30491  cdleme20c  30500  cdleme20k  30508  cdleme21a  30514  cdleme21b  30515  cdleme21c  30516  cdleme21h  30523  cdleme22b  30530  cdleme22d  30532  cdleme22f  30535  cdleme25a  30542  cdleme25c  30544  cdleme25dN  30545  cdleme26ee  30549  cdleme30a  30567  cdlemefr29bpre0N  30595  cdlemefr29clN  30596  cdlemefr32fvaN  30598  cdlemefr32fva1  30599  cdlemefs29bpre0N  30605  cdlemefs29bpre1N  30606  cdlemefs29cpre1N  30607  cdlemefs29clN  30608  cdleme43fsv1snlem  30609  cdlemefs32fvaN  30611  cdlemefs32fva1  30612  cdlemefs31fv1  30613  cdleme36a  30649  cdleme39a  30654  cdleme42a  30660  cdleme42c  30661  cdleme17d3  30685  cdleme48fv  30688  cdleme48bw  30691  cdleme48b  30692  cdlemeg46rgv  30717  cdlemeg46req  30718  cdlemeg46gfv  30719  cdleme48d  30724  cdleme50trn2a  30739  cdleme50trn2  30740  cdleme50ltrn  30746  cdlemf1  30750  cdlemf  30752  trlord  30758  cdlemg2dN  30779  cdlemg2fvlem  30783  cdlemg2l  30792  cdlemg7fvbwN  30796  cdlemg7aN  30814  cdlemg10bALTN  30825  cdlemg10c  30828  cdlemg17a  30850  cdlemg17dALTN  30853  cdlemg31b0a  30884  cdlemg31a  30886  cdlemg31b  30887  cdlemg34  30901  cdlemg36  30903  ltrnco  30908  trlcoabs2N  30911  trlcolem  30915  cdlemg48  30926  tgrpov  30937  tendoco2  30957  tendoplco2  30968  cdlemh1  31004  cdlemi1  31007  cdlemi2  31008  cdlemj3  31012  tendoid0  31014  cdlemk1  31020  cdlemk2  31021  cdlemk4  31023  cdlemk8  31027  cdlemk9  31028  cdlemk9bN  31029  cdlemk10  31032  cdlemk26b-3  31094  cdlemk26-3  31095  cdlemk28-3  31097  cdlemk37  31103  cdlemk39  31105  cdlemkfid1N  31110  cdlemkid1  31111  cdlemky  31115  cdlemkyu  31116  cdlemk19ylem  31119  cdlemk19xlem  31131  cdlemk11t  31135  cdlemk51  31142  cdlemkyyN  31151  cdleml6  31170  cdleml7  31171  cdleml8  31172  cdleml9  31173  erngdvlem4  31180  erngdvlem4-rN  31188  tendospcanN  31213  dia11N  31238  cdlemm10N  31308  dib11N  31350  dicvaddcl  31380  dicvscacl  31381  cdlemn6  31392  dihvalcq2  31437  dihopelvalcpre  31438  dihord6b  31450  dihord5apre  31452  dihmeetlem1N  31480  dihmeetlem2N  31489  dihglbcpreN  31490  dihjatc1  31501  dihmeetlem20N  31516  dih1dimatlem0  31518  dihatlat  31524  dihglblem6  31530  dochexmidlem4  31653  mapdpglem32  31895  mapdh8ad  31969  mapdh9aOLDN  31981  hdmap11lem2  32035  hdmap14lem6  32066
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator