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  7626  addcanprleml  7981  addcanprlemu  7982  ltmprr  8009  lelttrdi  8754  ixxdisj  10307  ixxss1  10308  ixxss2  10309  ixxss12  10310  iccss2  10348  iocssre  10357  icossre  10358  iccssre  10359  icodisj  10396  iccf1o  10409  fzen  10449  ioom  10697  intfracq  10759  flqdiv  10760  mulqaddmodid  10803  modsumfzodifsn  10835  addmodlteq  10837  remul  11639  sumtp  12183  crth  13004  phimullem  13005  eulerthlem1  13007  eulerthlemfi  13008  eulerthlemrprm  13009  eulerthlema  13010  eulerthlemh  13011  eulerthlemth  13012  ballotfilemcdc  13225  ballotfilemfc0  13234  ballotfilemro  13268  ctiunct  13333  strsetsid  13387  strleund  13459  strext  13461  mhmf  13774  submss  13785  eqger  14029  eqgcpbl  14033  lmodvscl  14643  lssssg  14699  rnglidlmsgrp  14836  2idlcpblrng  14862  lmfpm  15346  lmff  15352  lmtopcnp  15353  xmeter  15539  tgqioo  15658  ivthinclemlopn  15739  ivthinclemuopn  15741  limcimolemlt  15767  limcresi  15769  cosordlem  15953  relogbval  16059  relogbzcl  16060  nnlogbexp  16067  perfectlem2  16120  wlkprop  16580  wlkf  16583  wlkfg  16584  wlkvtxiedg  16598  wlk1walkdom  16612  wlkvtxedg  16616  upgr2wlkdc  16630  isclwwlkng  16659  eupthseg  16705  trlsegvdeglem3  16715  trlsegvdeglem5  16717  depindlem2  16760  depindlem3  16761