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  6883  resixp  7015  exmidapne  7626  addcanprleml  7981  addcanprlemu  7982  ltmprr  8009  lelttrdi  8754  ixxdisj  10307  ixxss1  10308  ixxss2  10309  ixxss12  10310  iccsupr  10370  icodisj  10396  ioom  10697  elicore  10703  intfracq  10759  flqdiv  10760  mulqaddmodid  10803  modsumfzodifsn  10835  seqf1oglem2  10959  cjmul  11652  sumtp  12183  crth  13004  eulerthlem1  13007  eulerthlemh  13011  eulerthlemth  13012  4sqlem13m  13184  ballotfilemro  13268  ennnfonelemim  13317  ctiunct  13333  strsetsid  13387  strleund  13459  strext  13461  mhm0  13777  submcl  13788  submmnd  13789  eqger  14029  eqgcpbl  14033  lmodvsdir  14651  lssclg  14703  rnglidlmsgrp  14836  2idlcpblrng  14862  lmcvg  15320  lmff  15352  lmtopcnp  15353  xmeter  15539  xmetresbl  15543  tgqioo  15658  ivthinclemlopn  15739  ivthinclemuopn  15741  limccl  15762  limcdifap  15765  limcresi  15769  limccnpcntop  15778  limccnp2lem  15779  limccnp2cntop  15780  limccoap  15781  cosordlem  15953  relogbval  16059  relogbzcl  16060  nnlogbexp  16067  birthdaylem3  16095  mersenne  16117  perfectlem2  16120  subgruhgredgdm  16523  wlk1walkdom  16612  upgr2wlkdc  16630  clwwlknon  16682  clwwlknonex2lem2  16691  depindlem2  16760  depindlem3  16761  depind  16762