Theorem simp1d 1011

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

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  simp1bi  1014  erinxp  6668  exmidapne  7327  addcanprleml  7681  addcanprlemu  7682  ltmprr  7709  lelttrdi  8453  ixxdisj  9978  ixxss1  9979  ixxss2  9980  ixxss12  9981  iccss2  10019  iocssre  10028  icossre  10029  iccssre  10030  icodisj  10067  iccf1o  10079  fzen  10118  ioom  10350  intfracq  10412  flqdiv  10413  mulqaddmodid  10456  modsumfzodifsn  10488  addmodlteq  10490  remul  11037  sumtp  11579  crth  12392  phimullem  12393  eulerthlem1  12395  eulerthlemfi  12396  eulerthlemrprm  12397  eulerthlema  12398  eulerthlemh  12399  eulerthlemth  12400  ctiunct  12657  strsetsid  12711  strleund  12781  strext  12783  mhmf  13097  submss  13108  eqger  13354  eqgcpbl  13358  lmodvscl  13861  lssssg  13916  rnglidlmsgrp  14053  2idlcpblrng  14079  lmfpm  14479  lmff  14485  lmtopcnp  14486  xmeter  14672  tgqioo  14791  ivthinclemlopn  14872  ivthinclemuopn  14874  limcimolemlt  14900  limcresi  14902  cosordlem  15085  relogbval  15187  relogbzcl  15188  nnlogbexp  15195  perfectlem2  15236