Theorem simp3d 1013

Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)

Hypothesis

Ref	Expression
3simp1d.1	⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))

Assertion

Ref	Expression
simp3d	⊢ (𝜑 → 𝜃)

Proof of Theorem simp3d

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
2		simp3 1001	. 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  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  simp3bi  1016  erinxp  6677  resixp  6801  exmidapne  7345  addcanprleml  7700  addcanprlemu  7701  ltmprr  7728  lelttrdi  8472  ixxdisj  9997  ixxss1  9998  ixxss2  9999  ixxss12  10000  iccsupr  10060  icodisj  10086  ioom  10369  elicore  10375  intfracq  10431  flqdiv  10432  mulqaddmodid  10475  modsumfzodifsn  10507  seqf1oglem2  10631  cjmul  11069  sumtp  11598  crth  12419  eulerthlem1  12422  eulerthlemh  12426  eulerthlemth  12427  4sqlem13m  12599  ennnfonelemim  12668  ctiunct  12684  strsetsid  12738  strleund  12808  strext  12810  mhm0  13172  submcl  13183  submmnd  13184  eqger  13432  eqgcpbl  13436  lmodvsdir  13946  lssclg  13998  rnglidlmsgrp  14131  2idlcpblrng  14157  lmcvg  14539  lmff  14571  lmtopcnp  14572  xmeter  14758  xmetresbl  14762  tgqioo  14877  ivthinclemlopn  14958  ivthinclemuopn  14960  limccl  14981  limcdifap  14984  limcresi  14988  limccnpcntop  14997  limccnp2lem  14998  limccnp2cntop  14999  limccoap  15000  cosordlem  15171  relogbval  15273  relogbzcl  15274  nnlogbexp  15281  mersenne  15319  perfectlem2  15322