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 )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1009

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 1011

This theorem is referenced by:  fidifsnen  7162  ordiso2  7365  ctssdc  7443  addlocpr  7893  xltadd1  10257  nn0ltexp2  11125  hashun  11223  fimaxq  11248  xrmaxltsup  12002  dvdslegcd  12719  lcmledvds  12826  divgcdcoprm0  12857  rpexp  12909  qexpz  13109  dfgrp3mlem  13880  gsumconstcmn  14143  rhmdvdsr  14455  rnglidlmcl  14789  iscnp4  15242  cnconst2  15257  blssps  15451  blss  15452  metcnp  15536  addcncntoplem  15585  cdivcncfap  15628  lgsfvalg  16038  lgsmod  16059  lgsdir  16068  lgsne0  16071  clwwlknonex2  16594  eulerpathum  16636