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  6636  exmidapne  7290  addcanprleml  7644  addcanprlemu  7645  ltmprr  7672  lelttrdi  8414  ixxdisj  9935  ixxss1  9936  ixxss2  9937  ixxss12  9938  iccss2  9976  iocssre  9985  icossre  9986  iccssre  9987  icodisj  10024  iccf1o  10036  fzen  10075  ioom  10293  intfracq  10353  flqdiv  10354  mulqaddmodid  10397  modsumfzodifsn  10429  addmodlteq  10431  remul  10916  sumtp  11457  crth  12259  phimullem  12260  eulerthlem1  12262  eulerthlemfi  12263  eulerthlemrprm  12264  eulerthlema  12265  eulerthlemh  12266  eulerthlemth  12267  ctiunct  12494  strsetsid  12548  strleund  12618  strext  12620  mhmf  12932  submss  12943  eqger  13180  eqgcpbl  13184  lmodvscl  13638  lssssg  13693  rnglidlmsgrp  13830  2idlcpblrng  13855  lmfpm  14220  lmff  14226  lmtopcnp  14227  xmeter  14413  tgqioo  14524  ivthinclemlopn  14591  ivthinclemuopn  14593  limcimolemlt  14610  limcresi  14612  cosordlem  14747  relogbval  14846  relogbzcl  14847  nnlogbexp  14854