Theorem simpll1 1060

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

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

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 1004

This theorem is referenced by:  fidifsnen  7040  ordiso2  7213  ctssdc  7291  addlocpr  7734  xltadd1  10084  nn0ltexp2  10943  hashun  11039  fimaxq  11062  xrmaxltsup  11784  dvdslegcd  12500  lcmledvds  12607  divgcdcoprm0  12638  rpexp  12690  qexpz  12890  dfgrp3mlem  13646  rhmdvdsr  14154  rnglidlmcl  14459  iscnp4  14907  cnconst2  14922  blssps  15116  blss  15117  metcnp  15201  addcncntoplem  15250  cdivcncfap  15293  lgsfvalg  15699  lgsmod  15720  lgsdir  15729  lgsne0  15732