Theorem 3ad2ant3 1047

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 1042	1 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  simp3l  1052  simp3r  1053  simp31  1060  simp32  1061  simp33  1062  simp3ll  1095  simp3lr  1096  simp3rl  1097  simp3rr  1098  simp3l1  1129  simp3l2  1130  simp3l3  1131  simp3r1  1132  simp3r2  1133  simp3r3  1134  simp31l  1147  simp31r  1148  simp32l  1149  simp32r  1150  simp33l  1151  simp33r  1152  simp311  1171  simp312  1172  simp313  1173  simp321  1174  simp322  1175  simp323  1176  simp331  1177  simp332  1178  simp333  1179  3anim123i  1211  3jaao  1345  ceqsalt  2840  ceqsralt  2841  vtoclgft  2865  ifbothdc  3657  ifnebibdc  3668  ssprsseq  3856  tpssi  3863  sotricim  4444  elirr  4663  en2lp  4676  reg3exmidlemwe  4701  sotri2  5160  poltletr  5163  funprg  5406  funtpg  5407  fntpg  5412  funimaexglem  5439  fvun1  5743  ftpg  5868  fsnunf  5884  fsnunfv  5885  caovimo  6248  funsssuppss  6458  brtposg  6485  smoel  6531  rdgivallem  6612  frecsuclem  6637  domssr  7017  mapxpen  7101  unsnfi  7179  unsnfidcex  7180  unsnfidcel  7181  sbthlemi4  7230  elfir  7260  updjud  7373  ltsopi  7635  distrnqg  7702  ltmnqg  7716  mulcanenq0ec  7760  distrnq0  7774  prarloclem5  7815  1idprl  7905  1idpru  7906  ltaprg  7934  recexprlemopl  7940  recexprlemopu  7942  recexprlem1ssl  7948  aptipr  7956  ltmprr  7957  cauappcvgprlemlol  7962  cauappcvgprlemupu  7964  caucvgprlemlol  7985  caucvgprlemupu  7987  caucvgprprlemlol  8013  caucvgprprlemupu  8015  readdcan  8413  cnegexlem2  8449  addcan2  8454  ltadd2  8693  apreap  8861  ltmul1  8866  apcotr  8881  apadd1  8882  mulext1  8886  divdirap  8971  divcanap5  8988  ltdiv1  9142  lt2halves  9474  zdivmul  9668  eluzsub  9884  ledivge1le  10059  addlelt  10101  xaddass  10202  xleadd1  10208  xltadd1  10209  elioo5  10266  iccsupr  10299  iccneg  10322  icoshft  10323  icoshftf1o  10324  zltaddlt1le  10341  fzen  10377  elfz1b  10424  fzrevral  10439  fzshftral  10442  elfz0ubfz0  10459  elfz0fzfz0  10460  fz0fzelfz0  10461  fz0fzdiffz0  10464  elfzo  10483  fzodcel  10487  elfzonlteqm1  10555  modqaddmulmod  10753  expdivap  10952  leexp2a  10954  bcval3  11113  omgadd  11166  ccatval1  11285  ccatval2  11286  ccatval3  11287  ccatass  11296  ccats1val2  11328  swrdval2  11343  swrdlen  11344  pfxfv  11376  pfxnd  11381  pfxsuffeqwrdeq  11390  swrdswrdlem  11396  swrdswrd  11397  pfxswrd  11398  pfxpfx  11400  ccats1pfxeq  11406  ccats1pfxeqrex  11407  pfxccatin12lem2  11423  pfxccatpfx1  11428  swrdccat3b  11432  pfxccatid  11433  shftfibg  11505  elicc4abs  11779  xrmaxltsup  11943  xrmaxadd  11946  xrlemininf  11956  xrminltinf  11957  mulcn2  11997  fsumsplitsnun  12105  prodfrecap  12232  demoivreALT  12460  dvdsval2  12476  dvdsmodexp  12481  dvdsmulcr  12507  modmulconst  12509  dvdsexp  12547  oddge22np1  12567  modremain  12615  mulgcd  12712  mulgcdr  12714  gcddiv  12715  rpmulgcd  12722  rplpwr  12723  coprmdvds  12789  cncongr1  12800  dvdsnprmd  12822  prmexpb  12848  rpexp  12850  cncongrprm  12854  modprm0  12952  modprmn0modprm0  12954  coprimeprodsq  12955  pythagtriplem1  12963  pythagtriplem3  12965  pythagtriplem10  12967  pythagtriplem6  12968  pythagtriplem11  12972  pythagtriplem12  12973  pythagtriplem13  12974  pythagtriplem15  12976  pythagtriplem17  12978  pythagtriplem19  12980  pcdvdsb  13018  dvdsprmpweqle  13035  pcfaclem  13047  isstructr  13227  setsvala  13243  setsresg  13250  strle3g  13321  imasaddvallemg  13528  fvprif  13556  mgmsscl  13574  insubm  13698  dfgrp3mlem  13811  mulgdirlem  13870  mulgp1  13872  mulgmodid  13878  eqglact  13942  rngdi  14084  rngdir  14085  rmodislmodlem  14498  rmodislmod  14499  lssclg  14512  2idlcpblrng  14671  qusmulrng  14680  psrbagaddclfi  14825  clsss  14983  ntrcls0  14996  neiss  15015  neipsm  15019  cnpnei  15084  cncnp2m  15096  cnconst2  15098  sslm  15112  upxp  15137  txmetcn  15384  ptolemy  15689  sincosq1eq  15704  rplogbval  15810  rpcxplogb  15829  pellexlem1  15845  lgsdirprm  15907  lgsdirnn0  15920  gausslemma2dlem1a  15931  gausslemma2dlem3  15936  2lgslem1a1  15959  2lgsoddprmlem1  15978  2lgsoddprmlem2  15979  structiedg0val  16035  lpvtx  16074  incistruhgr  16085  upgredg2vtx  16143  upgredgpr  16144  ausgrumgrien  16165  ausgrusgrien  16166  ushgredgedg  16221  ushgredgedgloop  16223  uhgrissubgr  16256  egrsubgr  16258  0uhgrsubgr  16260  wlkvtxeledgg  16339  wlkeq  16349  wlkl1loop  16353  uspgr2wlkeq  16360  uspgr2wlkeq2  16361  wlkres  16374  loopclwwlkn1b  16414  clwwlkext2edg  16417  clwwlknonex2lem2  16433  clwwlknonex2  16434  clwwlknun  16436  eupth2lem3lem6fi  16466  findset  16715