Theorem simp3d 1038

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

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  simp3bi  1041  erinxp  6845  resixp  6970  exmidapne  7579  addcanprleml  7934  addcanprlemu  7935  ltmprr  7962  lelttrdi  8705  ixxdisj  10242  ixxss1  10243  ixxss2  10244  ixxss12  10245  iccsupr  10305  icodisj  10331  ioom  10627  elicore  10633  intfracq  10689  flqdiv  10690  mulqaddmodid  10733  modsumfzodifsn  10765  seqf1oglem2  10889  cjmul  11578  sumtp  12108  crth  12929  eulerthlem1  12932  eulerthlemh  12936  eulerthlemth  12937  4sqlem13m  13109  ennnfonelemim  13196  ctiunct  13212  strsetsid  13266  strleund  13337  strext  13339  mhm0  13702  submcl  13713  submmnd  13714  eqger  13962  eqgcpbl  13966  lmodvsdir  14509  lssclg  14561  rnglidlmsgrp  14694  2idlcpblrng  14720  lmcvg  15131  lmff  15163  lmtopcnp  15164  xmeter  15350  xmetresbl  15354  tgqioo  15469  ivthinclemlopn  15550  ivthinclemuopn  15552  limccl  15573  limcdifap  15576  limcresi  15580  limccnpcntop  15589  limccnp2lem  15590  limccnp2cntop  15591  limccoap  15592  cosordlem  15763  relogbval  15865  relogbzcl  15866  nnlogbexp  15873  mersenne  15914  perfectlem2  15917  subgruhgredgdm  16314  wlk1walkdom  16403  upgr2wlkdc  16421  clwwlknon  16473  clwwlknonex2lem2  16482  depindlem2  16551  depindlem3  16552  depind  16553