Theorem simpll1 1036

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 1000	. 2 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ph )
2	1	adantr 276	1 |- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ph )

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

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 980

This theorem is referenced by:  fidifsnen  6872  ordiso2  7036  ctssdc  7114  addlocpr  7537  xltadd1  9878  nn0ltexp2  10691  hashun  10787  fimaxq  10809  xrmaxltsup  11268  dvdslegcd  11967  lcmledvds  12072  divgcdcoprm0  12103  rpexp  12155  qexpz  12352  dfgrp3mlem  12973  iscnp4  13757  cnconst2  13772  blssps  13966  blss  13967  metcnp  14051  addcncntoplem  14090  cdivcncfap  14126  lgsfvalg  14445  lgsmod  14466  lgsdir  14475  lgsne0  14478