Theorem simp1d 1036

Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)

Hypothesis

Ref	Expression
3simp1d.1	⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))

Assertion

Ref	Expression
simp1d	⊢ (𝜑 → 𝜓)

Proof of Theorem simp1d

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
2		simp1 1024	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ w3a 1005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  simp1bi  1039  erinxp  6842  exmidapne  7570  addcanprleml  7925  addcanprlemu  7926  ltmprr  7953  lelttrdi  8696  ixxdisj  10232  ixxss1  10233  ixxss2  10234  ixxss12  10235  iccss2  10273  iocssre  10282  icossre  10283  iccssre  10284  icodisj  10321  iccf1o  10334  fzen  10373  ioom  10616  intfracq  10678  flqdiv  10679  mulqaddmodid  10722  modsumfzodifsn  10754  addmodlteq  10756  remul  11550  sumtp  12093  crth  12914  phimullem  12915  eulerthlem1  12917  eulerthlemfi  12918  eulerthlemrprm  12919  eulerthlema  12920  eulerthlemh  12921  eulerthlemth  12922  ctiunct  13180  strsetsid  13234  strleund  13305  strext  13307  mhmf  13667  submss  13678  eqger  13930  eqgcpbl  13934  lmodvscl  14440  lssssg  14495  rnglidlmsgrp  14632  2idlcpblrng  14658  lmfpm  15095  lmff  15101  lmtopcnp  15102  xmeter  15288  tgqioo  15407  ivthinclemlopn  15488  ivthinclemuopn  15490  limcimolemlt  15516  limcresi  15518  cosordlem  15701  relogbval  15803  relogbzcl  15804  nnlogbexp  15811  perfectlem2  15855  wlkprop  16309  wlkf  16312  wlkfg  16313  wlkvtxiedg  16327  wlk1walkdom  16341  wlkvtxedg  16345  upgr2wlkdc  16359  isclwwlkng  16388  eupthseg  16434  trlsegvdeglem3  16444  trlsegvdeglem5  16446  depindlem2  16489  depindlem3  16490