Theorem simpll1 1036

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

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

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 980

This theorem is referenced by:  fidifsnen  6860  ordiso2  7024  ctssdc  7102  addlocpr  7510  xltadd1  9847  nn0ltexp2  10658  hashun  10753  fimaxq  10775  xrmaxltsup  11234  dvdslegcd  11932  lcmledvds  12037  divgcdcoprm0  12068  rpexp  12120  qexpz  12317  dfgrp3mlem  12829  iscnp4  13289  cnconst2  13304  blssps  13498  blss  13499  metcnp  13583  addcncntoplem  13622  cdivcncfap  13658  lgsfvalg  13977  lgsmod  13998  lgsdir  14007  lgsne0  14010