Theorem simpll1 1067

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  fidifsnen  7172  ordiso2  7376  ctssdc  7454  addlocpr  7904  xltadd1  10289  nn0ltexp2  11163  hashun  11261  fimaxq  11286  xrmaxltsup  12043  dvdslegcd  12760  lcmledvds  12867  divgcdcoprm0  12898  rpexp  12951  qexpz  13154  dfgrp3mlem  13956  gsumconstcmn  14250  rhmdvdsr  14566  rnglidlmcl  14901  iscnp4  15410  cnconst2  15425  blssps  15619  blss  15620  metcnp  15704  addcncntoplem  15753  cdivcncfap  15796  lgsfvalg  16290  lgsmod  16311  lgsdir  16320  lgsne0  16323  clwwlknonex2  16846  eulerpathum  16888