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  7178  ordiso2  7381  ctssdc  7459  addlocpr  7909  xltadd1  10294  nn0ltexp2  11168  hashun  11266  fimaxq  11291  xrmaxltsup  12048  dvdslegcd  12765  lcmledvds  12872  divgcdcoprm0  12903  rpexp  12956  qexpz  13159  dfgrp3mlem  13961  gsumconstcmn  14265  rhmdvdsr  14590  rnglidlmcl  14925  iscnp4  15461  cnconst2  15476  blssps  15670  blss  15671  metcnp  15755  addcncntoplem  15804  cdivcncfap  15847  lgsfvalg  16346  lgsmod  16367  lgsdir  16376  lgsne0  16379  clwwlknonex2  16902  eulerpathum  16944