Theorem simp1d 1040

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simp1bi  1043  erinxp  6887  exmidapne  7633  addcanprleml  7988  addcanprlemu  7989  ltmprr  8016  lelttrdi  8762  ixxdisj  10323  ixxss1  10324  ixxss2  10325  ixxss12  10326  iccss2  10364  iocssre  10373  icossre  10374  iccssre  10375  icodisj  10412  iccf1o  10425  fzen  10465  ioom  10713  intfracq  10779  flqdiv  10780  mulqaddmodid  10823  modsumfzodifsn  10855  addmodlteq  10857  remul  11660  sumtp  12207  crth  13032  phimullem  13033  eulerthlem1  13035  eulerthlemfi  13036  eulerthlemrprm  13037  eulerthlema  13038  eulerthlemh  13039  eulerthlemth  13040  ballotfilemcdc  13282  ballotfilemfc0  13291  ballotfilemro  13325  ctiunct  13390  strsetsid  13444  strleund  13517  strext  13519  mhmf  13832  submss  13843  eqger  14087  eqgcpbl  14091  lmodvscl  14751  lssssg  14807  rnglidlmsgrp  14944  2idlcpblrng  14970  lmfpm  15481  lmff  15487  lmtopcnp  15488  xmeter  15674  tgqioo  15793  ivthinclemlopn  15874  ivthinclemuopn  15876  limcimolemlt  15902  limcresi  15904  cosordlem  16089  relogbval  16199  relogbzcl  16200  nnlogbexp  16207  perfectlem2  16312  wlkprop  16785  wlkf  16788  wlkfg  16789  wlkvtxiedg  16803  wlk1walkdom  16817  wlkvtxedg  16821  upgr2wlkdc  16835  isclwwlkng  16864  eupthseg  16910  trlsegvdeglem3  16920  trlsegvdeglem5  16922  depindlem2  16965  depindlem3  16966