Theorem simpl3l 1116

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simpl3l	|- ( ( ( ch /\ th /\ ( ph /\ ps ) ) /\ ta ) -> ph )

Proof of Theorem simpl3l

Step	Hyp	Ref	Expression
1		simp3l 1089	. 2 |- ( ( ch /\ th /\ ( ph /\ ps ) ) -> ph )
2	1	adantr 481	1 |- ( ( ( ch /\ th /\ ( ph /\ ps ) ) /\ ta ) -> ph )

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:  tfisi  7058  omopth2  7664  ltmul1a  10872  xaddass  12079  xlemul2a  12119  swrdsbslen  13448  dvdsadd2b  15028  pockthg  15610  psgnunilem4  17917  efgred  18161  ptbasin  21380  basqtop  21514  xrsmopn  22615  axpasch  25821  axcontlem4  25847  br4  31648  nosupbnd1lem3  31856  nosupbnd1lem4  31857  btwnintr  32126  btwnexch3  32127  btwnouttr2  32129  cgrxfr  32162  lineext  32183  btwnconn1lem13  32206  btwnconn1lem14  32207  btwnconn3  32210  brsegle  32215  brsegle2  32216  segleantisym  32222  outsideofeu  32238  lineunray  32254  lineelsb2  32255  cvrcmp  34570  atcvrj2b  34718  3dimlem3  34747  3dimlem3OLDN  34748  3dim3  34755  ps-1  34763  lplnnle2at  34827  2llnm3N  34855  lvolnle3at  34868  4atlem0a  34879  4atlem3  34882  4atlem3a  34883  lnatexN  35065  paddasslem8  35113  paddasslem9  35114  paddasslem10  35115  paddasslem12  35117  paddasslem13  35118  lhp2lt  35287  lhpexle2lem  35295  lhpexle3  35298  lhpmcvr3  35311  lhpat3  35332  4atex  35362  trlval2  35450  ltrnideq  35462  ltrnatlw  35470  trlnle  35473  trlval4  35475  cdlemd4  35488  cdlemd5  35489  cdleme16  35572  cdleme21  35625  cdleme21k  35626  cdleme27cl  35654  cdleme27N  35657  cdleme29ex  35662  cdleme43fsv1snlem  35708  cdleme40m  35755  cdleme46f2g2  35781  cdleme46f2g1  35782  trlord  35857  cdlemg8  35919  cdlemg15a  35943  cdlemg16z  35947  cdlemg18a  35966  cdlemg24  35976  cdlemg38  36003  cdlemg40  36005  trlcone  36016  cdlemj2  36110  tendoid0  36113  tendoconid  36117  cdlemk34  36198  cdlemk38  36203  cdlemkid4  36222  cdlemk35s-id  36226  cdlemk39s-id  36228  cdlemk53  36245  tendospcanN  36312  cdlemm10N  36407  dihvalcqpre  36524  dihopelvalcpre  36537  dihord5b  36548  dihglblem5apreN  36580  dihmeetlem16N  36611  dihmeetlem17N  36612  dvh3dim3N  36738  qirropth  37473  mzpcong  37539  jm2.26  37569  aomclem6  37629  limcleqr  39876  fourierdlem42  40366