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  6677  exmidapne  7345  addcanprleml  7700  addcanprlemu  7701  ltmprr  7728  lelttrdi  8472  ixxdisj  9997  ixxss1  9998  ixxss2  9999  ixxss12  10000  iccss2  10038  iocssre  10047  icossre  10048  iccssre  10049  icodisj  10086  iccf1o  10098  fzen  10137  ioom  10369  intfracq  10431  flqdiv  10432  mulqaddmodid  10475  modsumfzodifsn  10507  addmodlteq  10509  remul  11056  sumtp  11598  crth  12419  phimullem  12420  eulerthlem1  12422  eulerthlemfi  12423  eulerthlemrprm  12424  eulerthlema  12425  eulerthlemh  12426  eulerthlemth  12427  ctiunct  12684  strsetsid  12738  strleund  12808  strext  12810  mhmf  13169  submss  13180  eqger  13432  eqgcpbl  13436  lmodvscl  13939  lssssg  13994  rnglidlmsgrp  14131  2idlcpblrng  14157  lmfpm  14587  lmff  14593  lmtopcnp  14594  xmeter  14780  tgqioo  14899  ivthinclemlopn  14980  ivthinclemuopn  14982  limcimolemlt  15008  limcresi  15010  cosordlem  15193  relogbval  15295  relogbzcl  15296  nnlogbexp  15303  perfectlem2  15344