Theorem simpll1 1067

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  fidifsnen  7172  ordiso2  7375  ctssdc  7453  addlocpr  7903  xltadd1  10278  nn0ltexp2  11147  hashun  11245  fimaxq  11270  xrmaxltsup  12024  dvdslegcd  12741  lcmledvds  12848  divgcdcoprm0  12879  rpexp  12931  qexpz  13131  dfgrp3mlem  13903  gsumconstcmn  14166  rhmdvdsr  14482  rnglidlmcl  14817  iscnp4  15319  cnconst2  15334  blssps  15528  blss  15529  metcnp  15613  addcncntoplem  15662  cdivcncfap  15705  lgsfvalg  16124  lgsmod  16145  lgsdir  16154  lgsne0  16157  clwwlknonex2  16680  eulerpathum  16722