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  10288  nn0ltexp2  11161  hashun  11259  fimaxq  11284  xrmaxltsup  12040  dvdslegcd  12757  lcmledvds  12864  divgcdcoprm0  12895  rpexp  12948  qexpz  13151  dfgrp3mlem  13952  gsumconstcmn  14215  rhmdvdsr  14531  rnglidlmcl  14866  iscnp4  15368  cnconst2  15383  blssps  15577  blss  15578  metcnp  15662  addcncntoplem  15711  cdivcncfap  15754  lgsfvalg  16222  lgsmod  16243  lgsdir  16252  lgsne0  16255  clwwlknonex2  16778  eulerpathum  16820