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  7056  ordiso2  7233  ctssdc  7311  addlocpr  7755  xltadd1  10110  nn0ltexp2  10970  hashun  11067  fimaxq  11090  xrmaxltsup  11818  dvdslegcd  12534  lcmledvds  12641  divgcdcoprm0  12672  rpexp  12724  qexpz  12924  dfgrp3mlem  13680  rhmdvdsr  14188  rnglidlmcl  14493  iscnp4  14941  cnconst2  14956  blssps  15150  blss  15151  metcnp  15235  addcncntoplem  15284  cdivcncfap  15327  lgsfvalg  15733  lgsmod  15754  lgsdir  15763  lgsne0  15766  clwwlknonex2  16289