Theorem simpll1 1031

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

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

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 975

This theorem is referenced by:  fidifsnen  6848  ordiso2  7012  ctssdc  7090  addlocpr  7498  xltadd1  9833  nn0ltexp2  10644  hashun  10740  fimaxq  10762  xrmaxltsup  11221  dvdslegcd  11919  lcmledvds  12024  divgcdcoprm0  12055  rpexp  12107  qexpz  12304  iscnp4  13012  cnconst2  13027  blssps  13221  blss  13222  metcnp  13306  addcncntoplem  13345  cdivcncfap  13381  lgsfvalg  13700  lgsmod  13721  lgsdir  13730  lgsne0  13733