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  6966  ordiso2  7136  ctssdc  7214  addlocpr  7648  xltadd1  9997  nn0ltexp2  10852  hashun  10948  fimaxq  10970  xrmaxltsup  11540  dvdslegcd  12256  lcmledvds  12363  divgcdcoprm0  12394  rpexp  12446  qexpz  12646  dfgrp3mlem  13401  rhmdvdsr  13908  rnglidlmcl  14213  iscnp4  14661  cnconst2  14676  blssps  14870  blss  14871  metcnp  14955  addcncntoplem  15004  cdivcncfap  15047  lgsfvalg  15453  lgsmod  15474  lgsdir  15483  lgsne0  15486