Theorem 3ad2ant3 964

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 271	. 2 ⊢ ((𝜃 ∧ 𝜑) → 𝜒)
3	2	3adant1 959	1 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 922

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-3an 924

This theorem is referenced by:  simp3l  969  simp3r  970  simp31  977  simp32  978  simp33  979  simp3ll  1012  simp3lr  1013  simp3rl  1014  simp3rr  1015  simp3l1  1046  simp3l2  1047  simp3l3  1048  simp3r1  1049  simp3r2  1050  simp3r3  1051  simp31l  1064  simp31r  1065  simp32l  1066  simp32r  1067  simp33l  1068  simp33r  1069  simp311  1088  simp312  1089  simp313  1090  simp321  1091  simp322  1092  simp323  1093  simp331  1094  simp332  1095  simp333  1096  3anim123i  1126  3jaao  1242  ceqsalt  2639  ceqsralt  2640  vtoclgft  2663  ifbothdc  3409  tpssi  3586  sotricim  4124  elirr  4330  en2lp  4343  reg3exmidlemwe  4367  sotri2  4796  poltletr  4799  funprg  5029  funtpg  5030  fntpg  5035  funimaexglem  5062  fvun1  5333  ftpg  5444  fsnunf  5459  fsnunfv  5460  caovimo  5795  brtposg  5973  smoel  6019  rdgivallem  6100  frecsuclem  6125  mapxpen  6516  unsnfi  6581  unsnfidcex  6582  unsnfidcel  6583  sbthlemi4  6613  updjud  6717  ltsopi  6823  distrnqg  6890  ltmnqg  6904  mulcanenq0ec  6948  distrnq0  6962  prarloclem5  7003  1idprl  7093  1idpru  7094  ltaprg  7122  recexprlemopl  7128  recexprlemopu  7130  recexprlem1ssl  7136  aptipr  7144  ltmprr  7145  cauappcvgprlemlol  7150  cauappcvgprlemupu  7152  caucvgprlemlol  7173  caucvgprlemupu  7175  caucvgprprlemlol  7201  caucvgprprlemupu  7203  readdcan  7566  cnegexlem2  7602  addcan2  7607  ltadd2  7841  apreap  8005  ltmul1  8010  apcotr  8025  apadd1  8026  mulext1  8030  divdirap  8103  divcanap5  8120  ltdiv1  8264  lt2halves  8584  zdivmul  8769  eluzsub  8980  ledivge1le  9135  addlelt  9171  elioo5  9283  iccsupr  9316  iccneg  9338  icoshft  9339  icoshftf1o  9340  zltaddlt1le  9355  fzen  9389  elfz1b  9434  fzrevral  9449  fzshftral  9452  elfz0ubfz0  9464  elfz0fzfz0  9465  fz0fzelfz0  9466  fz0fzdiffz0  9469  elfzo  9488  fzodcel  9491  elfzonlteqm1  9549  modqaddmulmod  9726  expdivap  9905  leexp2a  9907  bcval3  10056  omgadd  10107  shftfibg  10151  elicc4abs  10423  mulcn2  10595  dvdsval2  10681  dvdsmulcr  10708  modmulconst  10710  dvdsexp  10744  oddge22np1  10763  modremain  10811  mulgcd  10887  mulgcdr  10889  gcddiv  10890  rpmulgcd  10897  rplpwr  10898  coprmdvds  10956  cncongr1  10967  dvdsnprmd  10989  prmexpb  11012  rpexp  11014  cncongrprm  11018  findset  11285