Theorem simpll1 1062

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

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

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 1006

This theorem is referenced by:  fidifsnen  7059  ordiso2  7236  ctssdc  7314  addlocpr  7758  xltadd1  10113  nn0ltexp2  10974  hashun  11071  fimaxq  11094  xrmaxltsup  11838  dvdslegcd  12555  lcmledvds  12662  divgcdcoprm0  12693  rpexp  12745  qexpz  12945  dfgrp3mlem  13701  rhmdvdsr  14210  rnglidlmcl  14515  iscnp4  14968  cnconst2  14983  blssps  15177  blss  15178  metcnp  15262  addcncntoplem  15311  cdivcncfap  15354  lgsfvalg  15760  lgsmod  15781  lgsdir  15790  lgsne0  15793  clwwlknonex2  16316  eulerpathum  16358