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  7127  ordiso2  7328  ctssdc  7406  addlocpr  7853  xltadd1  10212  nn0ltexp2  11075  hashun  11173  fimaxq  11198  xrmaxltsup  11947  dvdslegcd  12664  lcmledvds  12771  divgcdcoprm0  12802  rpexp  12854  qexpz  13054  dfgrp3mlem  13828  rhmdvdsr  14337  rnglidlmcl  14645  iscnp4  15100  cnconst2  15115  blssps  15309  blss  15310  metcnp  15394  addcncntoplem  15443  cdivcncfap  15486  lgsfvalg  15895  lgsmod  15916  lgsdir  15925  lgsne0  15928  clwwlknonex2  16451  eulerpathum  16493