Theorem 3ad2ant3 1044

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

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  simp3l  1049  simp3r  1050  simp31  1057  simp32  1058  simp33  1059  simp3ll  1092  simp3lr  1093  simp3rl  1094  simp3rr  1095  simp3l1  1126  simp3l2  1127  simp3l3  1128  simp3r1  1129  simp3r2  1130  simp3r3  1131  simp31l  1144  simp31r  1145  simp32l  1146  simp32r  1147  simp33l  1148  simp33r  1149  simp311  1168  simp312  1169  simp313  1170  simp321  1171  simp322  1172  simp323  1173  simp331  1174  simp332  1175  simp333  1176  3anim123i  1208  3jaao  1342  ceqsalt  2827  ceqsralt  2828  vtoclgft  2852  ifbothdc  3638  ifnebibdc  3649  ssprsseq  3833  tpssi  3840  sotricim  4418  elirr  4637  en2lp  4650  reg3exmidlemwe  4675  sotri2  5132  poltletr  5135  funprg  5377  funtpg  5378  fntpg  5383  funimaexglem  5410  fvun1  5708  ftpg  5833  fsnunf  5849  fsnunfv  5850  caovimo  6211  brtposg  6415  smoel  6461  rdgivallem  6542  frecsuclem  6567  domssr  6946  mapxpen  7029  unsnfi  7104  unsnfidcex  7105  unsnfidcel  7106  sbthlemi4  7150  elfir  7163  updjud  7272  ltsopi  7530  distrnqg  7597  ltmnqg  7611  mulcanenq0ec  7655  distrnq0  7669  prarloclem5  7710  1idprl  7800  1idpru  7801  ltaprg  7829  recexprlemopl  7835  recexprlemopu  7837  recexprlem1ssl  7843  aptipr  7851  ltmprr  7852  cauappcvgprlemlol  7857  cauappcvgprlemupu  7859  caucvgprlemlol  7880  caucvgprlemupu  7882  caucvgprprlemlol  7908  caucvgprprlemupu  7910  readdcan  8309  cnegexlem2  8345  addcan2  8350  ltadd2  8589  apreap  8757  ltmul1  8762  apcotr  8777  apadd1  8778  mulext1  8782  divdirap  8867  divcanap5  8884  ltdiv1  9038  lt2halves  9370  zdivmul  9560  eluzsub  9776  ledivge1le  9951  addlelt  9993  xaddass  10094  xleadd1  10100  xltadd1  10101  elioo5  10158  iccsupr  10191  iccneg  10214  icoshft  10215  icoshftf1o  10216  zltaddlt1le  10232  fzen  10268  elfz1b  10315  fzrevral  10330  fzshftral  10333  elfz0ubfz0  10350  elfz0fzfz0  10351  fz0fzelfz0  10352  fz0fzdiffz0  10355  elfzo  10374  fzodcel  10378  elfzonlteqm1  10445  modqaddmulmod  10643  expdivap  10842  leexp2a  10844  bcval3  11003  omgadd  11055  ccatval1  11164  ccatval2  11165  ccatval3  11166  ccatass  11175  ccats1val2  11207  swrdval2  11222  swrdlen  11223  pfxfv  11255  pfxnd  11260  pfxsuffeqwrdeq  11269  swrdswrdlem  11275  swrdswrd  11276  pfxswrd  11277  pfxpfx  11279  ccats1pfxeq  11285  ccats1pfxeqrex  11286  pfxccatin12lem2  11302  pfxccatpfx1  11307  swrdccat3b  11311  pfxccatid  11312  shftfibg  11371  elicc4abs  11645  xrmaxltsup  11809  xrmaxadd  11812  xrlemininf  11822  xrminltinf  11823  mulcn2  11863  fsumsplitsnun  11970  prodfrecap  12097  demoivreALT  12325  dvdsval2  12341  dvdsmodexp  12346  dvdsmulcr  12372  modmulconst  12374  dvdsexp  12412  oddge22np1  12432  modremain  12480  mulgcd  12577  mulgcdr  12579  gcddiv  12580  rpmulgcd  12587  rplpwr  12588  coprmdvds  12654  cncongr1  12665  dvdsnprmd  12687  prmexpb  12713  rpexp  12715  cncongrprm  12719  modprm0  12817  modprmn0modprm0  12819  coprimeprodsq  12820  pythagtriplem1  12828  pythagtriplem3  12830  pythagtriplem10  12832  pythagtriplem6  12833  pythagtriplem11  12837  pythagtriplem12  12838  pythagtriplem13  12839  pythagtriplem15  12841  pythagtriplem17  12843  pythagtriplem19  12845  pcdvdsb  12883  dvdsprmpweqle  12900  pcfaclem  12912  isstructr  13087  setsvala  13103  setsresg  13110  strle3g  13181  imasaddvallemg  13388  fvprif  13416  mgmsscl  13434  insubm  13558  dfgrp3mlem  13671  mulgdirlem  13730  mulgp1  13732  mulgmodid  13738  eqglact  13802  rngdi  13943  rngdir  13944  rmodislmodlem  14354  rmodislmod  14355  lssclg  14368  2idlcpblrng  14527  qusmulrng  14536  clsss  14832  ntrcls0  14845  neiss  14864  neipsm  14868  cnpnei  14933  cncnp2m  14945  cnconst2  14947  sslm  14961  upxp  14986  txmetcn  15233  ptolemy  15538  sincosq1eq  15553  rplogbval  15659  rpcxplogb  15678  lgsdirprm  15753  lgsdirnn0  15766  gausslemma2dlem1a  15777  gausslemma2dlem3  15782  2lgslem1a1  15805  2lgsoddprmlem1  15824  2lgsoddprmlem2  15825  structiedg0val  15881  lpvtx  15920  incistruhgr  15931  upgredg2vtx  15987  upgredgpr  15988  ausgrumgrien  16009  ausgrusgrien  16010  ushgredgedg  16065  ushgredgedgloop  16067  wlkvtxeledgg  16141  wlkeq  16151  wlkl1loop  16155  uspgr2wlkeq  16162  uspgr2wlkeq2  16163  wlkres  16174  loopclwwlkn1b  16214  clwwlkext2edg  16217  clwwlknonex2lem2  16233  clwwlknonex2  16234  clwwlknun  16236  findset  16476