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  6926  ordiso2  7094  ctssdc  7172  addlocpr  7596  xltadd1  9942  nn0ltexp2  10780  hashun  10876  fimaxq  10898  xrmaxltsup  11401  dvdslegcd  12101  lcmledvds  12208  divgcdcoprm0  12239  rpexp  12291  qexpz  12490  dfgrp3mlem  13170  rhmdvdsr  13671  rnglidlmcl  13976  iscnp4  14386  cnconst2  14401  blssps  14595  blss  14596  metcnp  14680  addcncntoplem  14719  cdivcncfap  14758  lgsfvalg  15121  lgsmod  15142  lgsdir  15151  lgsne0  15154