Theorem simpll1 1039

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

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

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 983

This theorem is referenced by:  fidifsnen  6993  ordiso2  7163  ctssdc  7241  addlocpr  7684  xltadd1  10033  nn0ltexp2  10891  hashun  10987  fimaxq  11009  xrmaxltsup  11684  dvdslegcd  12400  lcmledvds  12507  divgcdcoprm0  12538  rpexp  12590  qexpz  12790  dfgrp3mlem  13545  rhmdvdsr  14052  rnglidlmcl  14357  iscnp4  14805  cnconst2  14820  blssps  15014  blss  15015  metcnp  15099  addcncntoplem  15148  cdivcncfap  15191  lgsfvalg  15597  lgsmod  15618  lgsdir  15627  lgsne0  15630