Theorem simp1d 1012

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

Syntax hints:   → wi 4   ∧ w3a 981

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 983

This theorem is referenced by:  simp1bi  1015  erinxp  6703  exmidapne  7379  addcanprleml  7734  addcanprlemu  7735  ltmprr  7762  lelttrdi  8506  ixxdisj  10032  ixxss1  10033  ixxss2  10034  ixxss12  10035  iccss2  10073  iocssre  10082  icossre  10083  iccssre  10084  icodisj  10121  iccf1o  10133  fzen  10172  ioom  10410  intfracq  10472  flqdiv  10473  mulqaddmodid  10516  modsumfzodifsn  10548  addmodlteq  10550  remul  11227  sumtp  11769  crth  12590  phimullem  12591  eulerthlem1  12593  eulerthlemfi  12594  eulerthlemrprm  12595  eulerthlema  12596  eulerthlemh  12597  eulerthlemth  12598  ctiunct  12855  strsetsid  12909  strleund  12979  strext  12981  mhmf  13341  submss  13352  eqger  13604  eqgcpbl  13608  lmodvscl  14111  lssssg  14166  rnglidlmsgrp  14303  2idlcpblrng  14329  lmfpm  14759  lmff  14765  lmtopcnp  14766  xmeter  14952  tgqioo  15071  ivthinclemlopn  15152  ivthinclemuopn  15154  limcimolemlt  15180  limcresi  15182  cosordlem  15365  relogbval  15467  relogbzcl  15468  nnlogbexp  15475  perfectlem2  15516