Theorem simpll1 1038

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

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

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 982

This theorem is referenced by:  fidifsnen  6928  ordiso2  7096  ctssdc  7174  addlocpr  7598  xltadd1  9945  nn0ltexp2  10783  hashun  10879  fimaxq  10901  xrmaxltsup  11404  dvdslegcd  12104  lcmledvds  12211  divgcdcoprm0  12242  rpexp  12294  qexpz  12493  dfgrp3mlem  13173  rhmdvdsr  13674  rnglidlmcl  13979  iscnp4  14397  cnconst2  14412  blssps  14606  blss  14607  metcnp  14691  addcncntoplem  14740  cdivcncfap  14783  lgsfvalg  15162  lgsmod  15183  lgsdir  15192  lgsne0  15195