Theorem simpll1 1038

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

Assertion

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

Proof of Theorem simpll1

Step	Hyp	Ref	Expression
1		simpl1 1002	. 2 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ph )
2	1	adantr 276	1 |- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ph )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  fidifsnen  6940  ordiso2  7110  ctssdc  7188  addlocpr  7620  xltadd1  9968  nn0ltexp2  10818  hashun  10914  fimaxq  10936  xrmaxltsup  11440  dvdslegcd  12156  lcmledvds  12263  divgcdcoprm0  12294  rpexp  12346  qexpz  12546  dfgrp3mlem  13300  rhmdvdsr  13807  rnglidlmcl  14112  iscnp4  14538  cnconst2  14553  blssps  14747  blss  14748  metcnp  14832  addcncntoplem  14881  cdivcncfap  14924  lgsfvalg  15330  lgsmod  15351  lgsdir  15360  lgsne0  15363