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  6883  exmidapne  7627  addcanprleml  7982  addcanprlemu  7983  ltmprr  8010  lelttrdi  8756  ixxdisj  10316  ixxss1  10317  ixxss2  10318  ixxss12  10319  iccss2  10357  iocssre  10366  icossre  10367  iccssre  10368  icodisj  10405  iccf1o  10418  fzen  10458  ioom  10706  intfracq  10772  flqdiv  10773  mulqaddmodid  10816  modsumfzodifsn  10848  addmodlteq  10850  remul  11653  sumtp  12200  crth  13025  phimullem  13026  eulerthlem1  13028  eulerthlemfi  13029  eulerthlemrprm  13030  eulerthlema  13031  eulerthlemh  13032  eulerthlemth  13033  ballotfilemcdc  13275  ballotfilemfc0  13284  ballotfilemro  13318  ctiunct  13383  strsetsid  13437  strleund  13510  strext  13512  mhmf  13825  submss  13836  eqger  14080  eqgcpbl  14084  lmodvscl  14725  lssssg  14781  rnglidlmsgrp  14918  2idlcpblrng  14944  lmfpm  15435  lmff  15441  lmtopcnp  15442  xmeter  15628  tgqioo  15747  ivthinclemlopn  15828  ivthinclemuopn  15830  limcimolemlt  15856  limcresi  15858  cosordlem  16043  relogbval  16153  relogbzcl  16154  nnlogbexp  16161  perfectlem2  16266  wlkprop  16739  wlkf  16742  wlkfg  16743  wlkvtxiedg  16757  wlk1walkdom  16771  wlkvtxedg  16775  upgr2wlkdc  16789  isclwwlkng  16818  eupthseg  16864  trlsegvdeglem3  16874  trlsegvdeglem5  16876  depindlem2  16919  depindlem3  16920