Theorem simp1d 1033

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

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  simp1bi  1036  erinxp  6769  exmidapne  7462  addcanprleml  7817  addcanprlemu  7818  ltmprr  7845  lelttrdi  8589  ixxdisj  10116  ixxss1  10117  ixxss2  10118  ixxss12  10119  iccss2  10157  iocssre  10166  icossre  10167  iccssre  10168  icodisj  10205  iccf1o  10217  fzen  10256  ioom  10497  intfracq  10559  flqdiv  10560  mulqaddmodid  10603  modsumfzodifsn  10635  addmodlteq  10637  remul  11404  sumtp  11946  crth  12767  phimullem  12768  eulerthlem1  12770  eulerthlemfi  12771  eulerthlemrprm  12772  eulerthlema  12773  eulerthlemh  12774  eulerthlemth  12775  ctiunct  13032  strsetsid  13086  strleund  13157  strext  13159  mhmf  13519  submss  13530  eqger  13782  eqgcpbl  13786  lmodvscl  14290  lssssg  14345  rnglidlmsgrp  14482  2idlcpblrng  14508  lmfpm  14938  lmff  14944  lmtopcnp  14945  xmeter  15131  tgqioo  15250  ivthinclemlopn  15331  ivthinclemuopn  15333  limcimolemlt  15359  limcresi  15361  cosordlem  15544  relogbval  15646  relogbzcl  15647  nnlogbexp  15654  perfectlem2  15695  wlkprop  16099  wlkf  16102  wlkfg  16103  wlkvtxiedg  16117  wlk1walkdom  16131  wlkvtxedg  16135  upgr2wlkdc  16147  isclwwlkng  16175