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  6756  exmidapne  7446  addcanprleml  7801  addcanprlemu  7802  ltmprr  7829  lelttrdi  8573  ixxdisj  10099  ixxss1  10100  ixxss2  10101  ixxss12  10102  iccss2  10140  iocssre  10149  icossre  10150  iccssre  10151  icodisj  10188  iccf1o  10200  fzen  10239  ioom  10480  intfracq  10542  flqdiv  10543  mulqaddmodid  10586  modsumfzodifsn  10618  addmodlteq  10620  remul  11383  sumtp  11925  crth  12746  phimullem  12747  eulerthlem1  12749  eulerthlemfi  12750  eulerthlemrprm  12751  eulerthlema  12752  eulerthlemh  12753  eulerthlemth  12754  ctiunct  13011  strsetsid  13065  strleund  13136  strext  13138  mhmf  13498  submss  13509  eqger  13761  eqgcpbl  13765  lmodvscl  14269  lssssg  14324  rnglidlmsgrp  14461  2idlcpblrng  14487  lmfpm  14917  lmff  14923  lmtopcnp  14924  xmeter  15110  tgqioo  15229  ivthinclemlopn  15310  ivthinclemuopn  15312  limcimolemlt  15338  limcresi  15340  cosordlem  15523  relogbval  15625  relogbzcl  15626  nnlogbexp  15633  perfectlem2  15674  wlkprop  16039  wlkf  16042  wlkfg  16043  wlkvtxiedg  16056  wlk1walkdom  16070  wlkvtxedg  16074