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  6898  ordiso2  7064  ctssdc  7142  addlocpr  7565  xltadd1  9906  nn0ltexp2  10721  hashun  10817  fimaxq  10839  xrmaxltsup  11298  dvdslegcd  11997  lcmledvds  12102  divgcdcoprm0  12133  rpexp  12185  qexpz  12384  dfgrp3mlem  13042  rhmdvdsr  13525  rnglidlmcl  13796  iscnp4  14175  cnconst2  14190  blssps  14384  blss  14385  metcnp  14469  addcncntoplem  14508  cdivcncfap  14544  lgsfvalg  14864  lgsmod  14885  lgsdir  14894  lgsne0  14897