Theorem 3ad2ant3 927

Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)

Hypothesis

Ref	Expression
3ad2ant.1	⊢ (𝜑 → 𝜒)

Assertion

Ref	Expression
3ad2ant3	⊢ ((𝜓 ∧ 𝜃 ∧ 𝜑) → 𝜒)

Proof of Theorem 3ad2ant3

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 ⊢ (𝜑 → 𝜒)
2	1	adantl 262	. 2 ⊢ ((𝜃 ∧ 𝜑) → 𝜒)
3	2	3adant1 922	1 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 885

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  simp3l  932  simp3r  933  simp31  940  simp32  941  simp33  942  simp3ll  975  simp3lr  976  simp3rl  977  simp3rr  978  simp3l1  1009  simp3l2  1010  simp3l3  1011  simp3r1  1012  simp3r2  1013  simp3r3  1014  simp31l  1027  simp31r  1028  simp32l  1029  simp32r  1030  simp33l  1031  simp33r  1032  simp311  1051  simp312  1052  simp313  1053  simp321  1054  simp322  1055  simp323  1056  simp331  1057  simp332  1058  simp333  1059  3anim123i  1089  3jaao  1203  ceqsalt  2580  ceqsralt  2581  vtoclgft  2604  ifbothdc  3357  tpssi  3530  sotricim  4060  elirr  4266  en2lp  4278  reg3exmidlemwe  4303  sotri2  4722  poltletr  4725  funprg  4949  funtpg  4950  fntpg  4955  funimaexglem  4982  fvun1  5239  ftpg  5347  fsnunf  5362  fsnunfv  5363  caovimo  5694  brtposg  5869  smoel  5915  rdgivallem  5968  frecsuclem1  5987  frecsuclemdm  5988  frecsuclem2  5989  frecsuclem3  5990  ltsopi  6418  distrnqg  6485  ltmnqg  6499  mulcanenq0ec  6543  distrnq0  6557  prarloclem5  6598  1idprl  6688  1idpru  6689  ltaprg  6717  recexprlemopl  6723  recexprlemopu  6725  recexprlem1ssl  6731  aptipr  6739  ltmprr  6740  cauappcvgprlemlol  6745  cauappcvgprlemupu  6747  caucvgprlemlol  6768  caucvgprlemupu  6770  caucvgprprlemlol  6796  caucvgprprlemupu  6798  readdcan  7153  cnegexlem2  7187  addcan2  7192  ltadd2  7416  apreap  7578  ltmul1  7583  apcotr  7598  apadd1  7599  mulext1  7603  divdirap  7674  divcanap5  7690  ltdiv1  7834  lt2halves  8160  zdivmul  8330  eluzsub  8502  ledivge1le  8652  elioo5  8802  iccsupr  8835  iccneg  8857  icoshft  8858  icoshftf1o  8859  fzen  8907  elfz1b  8952  fzrevral  8967  fzshftral  8970  elfz0ubfz0  8982  elfz0fzfz0  8983  fz0fzelfz0  8984  fz0fzdiffz0  8987  elfzo  9006  elfzonlteqm1  9066  expdivap  9305  leexp2a  9307  shftfibg  9421  elicc4abs  9690  mulcn2  9833  findset  10070