Theorem simp3d 1042

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simp3bi  1045  erinxp  6887  resixp  7020  exmidapne  7633  addcanprleml  7988  addcanprlemu  7989  ltmprr  8016  lelttrdi  8762  ixxdisj  10323  ixxss1  10324  ixxss2  10325  ixxss12  10326  iccsupr  10386  icodisj  10412  ioom  10713  elicore  10719  intfracq  10779  flqdiv  10780  mulqaddmodid  10823  modsumfzodifsn  10855  seqf1oglem2  10979  cjmul  11673  sumtp  12207  crth  13032  eulerthlem1  13035  eulerthlemh  13039  eulerthlemth  13040  4sqlem13m  13212  ballotfilemro  13325  ennnfonelemim  13374  ctiunct  13390  strsetsid  13444  strleund  13517  strext  13519  mhm0  13835  submcl  13846  submmnd  13847  eqger  14087  eqgcpbl  14091  lmodvsdir  14759  lssclg  14811  rnglidlmsgrp  14944  2idlcpblrng  14970  lmcvg  15455  lmff  15487  lmtopcnp  15488  xmeter  15674  xmetresbl  15678  tgqioo  15793  ivthinclemlopn  15874  ivthinclemuopn  15876  limccl  15897  limcdifap  15900  limcresi  15904  limccnpcntop  15913  limccnp2lem  15914  limccnp2cntop  15915  limccoap  15916  cosordlem  16089  relogbval  16199  relogbzcl  16200  nnlogbexp  16207  birthdaylem3  16239  ppiqsval  16252  chtqleppi  16306  mersenne  16309  perfectlem2  16312  subgruhgredgdm  16728  wlk1walkdom  16817  upgr2wlkdc  16835  clwwlknon  16887  clwwlknonex2lem2  16896  depindlem2  16965  depindlem3  16966  depind  16967