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  7343  addcanprleml  7698  addcanprlemu  7699  ltmprr  7726  lelttrdi  8470  ixxdisj  9995  ixxss1  9996  ixxss2  9997  ixxss12  9998  iccss2  10036  iocssre  10045  icossre  10046  iccssre  10047  icodisj  10084  iccf1o  10096  fzen  10135  ioom  10367  intfracq  10429  flqdiv  10430  mulqaddmodid  10473  modsumfzodifsn  10505  addmodlteq  10507  remul  11054  sumtp  11596  crth  12417  phimullem  12418  eulerthlem1  12420  eulerthlemfi  12421  eulerthlemrprm  12422  eulerthlema  12423  eulerthlemh  12424  eulerthlemth  12425  ctiunct  12682  strsetsid  12736  strleund  12806  strext  12808  mhmf  13167  submss  13178  eqger  13430  eqgcpbl  13434  lmodvscl  13937  lssssg  13992  rnglidlmsgrp  14129  2idlcpblrng  14155  lmfpm  14563  lmff  14569  lmtopcnp  14570  xmeter  14756  tgqioo  14875  ivthinclemlopn  14956  ivthinclemuopn  14958  limcimolemlt  14984  limcresi  14986  cosordlem  15169  relogbval  15271  relogbzcl  15272  nnlogbexp  15279  perfectlem2  15320