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  7622  xltadd1  9970  nn0ltexp2  10820  hashun  10916  fimaxq  10938  xrmaxltsup  11442  dvdslegcd  12158  lcmledvds  12265  divgcdcoprm0  12296  rpexp  12348  qexpz  12548  dfgrp3mlem  13302  rhmdvdsr  13809  rnglidlmcl  14114  iscnp4  14540  cnconst2  14555  blssps  14749  blss  14750  metcnp  14834  addcncntoplem  14883  cdivcncfap  14926  lgsfvalg  15332  lgsmod  15353  lgsdir  15362  lgsne0  15365