Theorem simpll1 1060

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

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

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 1004

This theorem is referenced by:  fidifsnen  7052  ordiso2  7225  ctssdc  7303  addlocpr  7746  xltadd1  10101  nn0ltexp2  10961  hashun  11058  fimaxq  11081  xrmaxltsup  11809  dvdslegcd  12525  lcmledvds  12632  divgcdcoprm0  12663  rpexp  12715  qexpz  12915  dfgrp3mlem  13671  rhmdvdsr  14179  rnglidlmcl  14484  iscnp4  14932  cnconst2  14947  blssps  15141  blss  15142  metcnp  15226  addcncntoplem  15275  cdivcncfap  15318  lgsfvalg  15724  lgsmod  15745  lgsdir  15754  lgsne0  15757  clwwlknonex2  16234