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  6967  ordiso2  7137  ctssdc  7215  addlocpr  7649  xltadd1  9998  nn0ltexp2  10854  hashun  10950  fimaxq  10972  xrmaxltsup  11569  dvdslegcd  12285  lcmledvds  12392  divgcdcoprm0  12423  rpexp  12475  qexpz  12675  dfgrp3mlem  13430  rhmdvdsr  13937  rnglidlmcl  14242  iscnp4  14690  cnconst2  14705  blssps  14899  blss  14900  metcnp  14984  addcncntoplem  15033  cdivcncfap  15076  lgsfvalg  15482  lgsmod  15503  lgsdir  15512  lgsne0  15515