Theorem simp1d 1011

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 999	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  simp1bi  1014  erinxp  6665  exmidapne  7322  addcanprleml  7676  addcanprlemu  7677  ltmprr  7704  lelttrdi  8447  ixxdisj  9972  ixxss1  9973  ixxss2  9974  ixxss12  9975  iccss2  10013  iocssre  10022  icossre  10023  iccssre  10024  icodisj  10061  iccf1o  10073  fzen  10112  ioom  10332  intfracq  10394  flqdiv  10395  mulqaddmodid  10438  modsumfzodifsn  10470  addmodlteq  10472  remul  11019  sumtp  11560  crth  12365  phimullem  12366  eulerthlem1  12368  eulerthlemfi  12369  eulerthlemrprm  12370  eulerthlema  12371  eulerthlemh  12372  eulerthlemth  12373  ctiunct  12600  strsetsid  12654  strleund  12724  strext  12726  mhmf  13040  submss  13051  eqger  13297  eqgcpbl  13301  lmodvscl  13804  lssssg  13859  rnglidlmsgrp  13996  2idlcpblrng  14022  lmfpm  14422  lmff  14428  lmtopcnp  14429  xmeter  14615  tgqioo  14734  ivthinclemlopn  14815  ivthinclemuopn  14817  limcimolemlt  14843  limcresi  14845  cosordlem  15025  relogbval  15124  relogbzcl  15125  nnlogbexp  15132