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

Theorem simp12l 1068
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp12l  |-  ( ( ( ch  /\  ( ph  /\  ps )  /\  th )  /\  ta  /\  et )  ->  ph )

Proof of Theorem simp12l
StepHypRef Expression
1 simp2l 981 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ph )
213ad2ant1 976 1  |-  ( ( ( ch  /\  ( ph  /\  ps )  /\  th )  /\  ta  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  ackbij1lem16  7861  axcontlem4  24595  prdnei  25573  mzpcong  27059  eqlkr  29289  athgt  29645  llncvrlpln2  29746  4atlem11b  29797  2lnat  29973  cdlemblem  29982  pclfinN  30089  lhp2lt  30190  lhpmcvr5N  30216  lhpmcvr6N  30217  lhp2at0  30221  lhp2atnle  30222  lhp2at0nle  30224  4atexlemex6  30263  cdlemd2  30388  cdlemd7  30393  cdlemd8  30394  cdlemd9  30395  cdleme7aa  30431  cdleme7c  30434  cdleme7d  30435  cdleme7e  30436  cdleme7ga  30437  cdleme7  30438  cdleme11c  30450  cdleme11dN  30451  cdleme11e  30452  cdleme11  30459  cdleme14  30462  cdleme15a  30463  cdleme15b  30464  cdleme15d  30466  cdleme15  30467  cdleme16b  30468  cdleme16c  30469  cdleme16d  30470  cdleme18d  30484  cdleme19b  30493  cdleme19e  30496  cdleme20d  30501  cdleme20g  30504  cdleme20h  30505  cdleme20i  30506  cdleme20j  30507  cdleme20l2  30510  cdleme20l  30511  cdleme20m  30512  cdleme21c  30516  cdleme21ct  30518  cdleme21d  30519  cdleme21e  30520  cdleme22cN  30531  cdleme22f  30535  cdleme22f2  30536  cdleme23a  30538  cdleme23b  30539  cdleme23c  30540  cdleme25a  30542  cdleme25dN  30545  cdleme26fALTN  30551  cdleme26f  30552  cdleme26f2ALTN  30553  cdleme26f2  30554  cdlemefr29bpre0N  30595  cdlemefr29clN  30596  cdlemefr32fvaN  30598  cdlemefr32fva1  30599  cdleme41sn3a  30622  cdleme32le  30636  cdleme35a  30637  cdleme35fnpq  30638  cdleme35b  30639  cdleme35c  30640  cdleme35d  30641  cdleme35e  30642  cdleme35f  30643  cdleme36a  30649  cdleme37m  30651  cdleme39n  30655  cdleme43bN  30679  cdleme43dN  30681  cdleme17d2  30684  cdlemeg46c  30702  cdlemeg46nlpq  30706  cdlemeg46ngfr  30707  cdlemeg46req  30718  cdlemeg46gfv  30719  cdleme50trn1  30738  cdleme50trn2a  30739  cdlemf1  30750  trlord  30758  cdlemb3  30795  cdlemg7fvbwN  30796  cdlemg7aN  30814  cdlemg10a  30829  cdlemg10  30830  cdlemg12d  30835  cdlemg12e  30836  cdlemg12f  30837  cdlemg12g  30838  cdlemg12  30839  cdlemg13a  30840  cdlemg13  30841  cdlemg17b  30851  cdlemg17f  30855  cdlemg17g  30856  cdlemg17h  30857  cdlemg17pq  30861  cdlemg17  30866  cdlemg19a  30872  cdlemg19  30873  cdlemg21  30875  cdlemg27a  30881  cdlemg27b  30885  cdlemg31c  30888  cdlemg33b0  30890  cdlemg33a  30895  trlcone  30917  cdlemg44  30922  cdlemg48  30926  cdlemk37  31103  cdlemky  31115  cdlemk11ta  31118  cdleml4N  31168  dihord1  31408  dihord2pre2  31416  dihord4  31448  dihord5apre  31452  dihmeetlem1N  31480  dihglblem3N  31485  dihglbcpreN  31490  dihmeetlem3N  31495  dihmeetlem13N  31509  mapdpglem32  31895  baerlem3lem2  31900  baerlem5alem2  31901  baerlem5blem2  31902
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