Theorem simpll1 1026

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

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  fidifsnen  6836  ordiso2  7000  ctssdc  7078  addlocpr  7477  xltadd1  9812  nn0ltexp2  10623  hashun  10718  fimaxq  10740  xrmaxltsup  11199  dvdslegcd  11897  lcmledvds  12002  divgcdcoprm0  12033  rpexp  12085  qexpz  12282  iscnp4  12858  cnconst2  12873  blssps  13067  blss  13068  metcnp  13152  addcncntoplem  13191  cdivcncfap  13227  lgsfvalg  13546  lgsmod  13567  lgsdir  13576  lgsne0  13579