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  7028  ordiso2  7198  ctssdc  7276  addlocpr  7719  xltadd1  10068  nn0ltexp2  10926  hashun  11022  fimaxq  11044  xrmaxltsup  11764  dvdslegcd  12480  lcmledvds  12587  divgcdcoprm0  12618  rpexp  12670  qexpz  12870  dfgrp3mlem  13626  rhmdvdsr  14133  rnglidlmcl  14438  iscnp4  14886  cnconst2  14901  blssps  15095  blss  15096  metcnp  15180  addcncntoplem  15229  cdivcncfap  15272  lgsfvalg  15678  lgsmod  15699  lgsdir  15708  lgsne0  15711