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  7100  ordiso2  7294  ctssdc  7372  addlocpr  7816  xltadd1  10172  nn0ltexp2  11034  hashun  11131  fimaxq  11154  xrmaxltsup  11898  dvdslegcd  12615  lcmledvds  12722  divgcdcoprm0  12753  rpexp  12805  qexpz  13005  dfgrp3mlem  13761  rhmdvdsr  14270  rnglidlmcl  14576  iscnp4  15029  cnconst2  15044  blssps  15238  blss  15239  metcnp  15323  addcncntoplem  15372  cdivcncfap  15415  lgsfvalg  15824  lgsmod  15845  lgsdir  15854  lgsne0  15857  clwwlknonex2  16380  eulerpathum  16422