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  7176  ordiso2  7381  ctssdc  7459  addlocpr  7909  xltadd1  10295  nn0ltexp2  11169  hashun  11267  fimaxq  11292  xrmaxltsup  12049  dvdslegcd  12766  lcmledvds  12873  divgcdcoprm0  12904  rpexp  12957  qexpz  13160  dfgrp3mlem  13962  gsumconstcmn  14266  rhmdvdsr  14591  rnglidlmcl  14926  iscnp4  15444  cnconst2  15459  blssps  15653  blss  15654  metcnp  15738  addcncntoplem  15787  cdivcncfap  15830  lgsfvalg  16329  lgsmod  16350  lgsdir  16359  lgsne0  16362  clwwlknonex2  16885  eulerpathum  16927