Theorem simpll1 1063

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

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

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 1007

This theorem is referenced by:  fidifsnen  7138  ordiso2  7339  ctssdc  7417  addlocpr  7867  xltadd1  10228  nn0ltexp2  11096  hashun  11194  fimaxq  11219  xrmaxltsup  11968  dvdslegcd  12685  lcmledvds  12792  divgcdcoprm0  12823  rpexp  12875  qexpz  13075  dfgrp3mlem  13853  rhmdvdsr  14420  rnglidlmcl  14754  iscnp4  15209  cnconst2  15224  blssps  15418  blss  15419  metcnp  15503  addcncntoplem  15552  cdivcncfap  15595  lgsfvalg  16004  lgsmod  16025  lgsdir  16034  lgsne0  16037  clwwlknonex2  16560  eulerpathum  16602