Theorem ad2ant2r 759

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)

Hypothesis

Ref	Expression
ad2ant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
ad2ant2r	⊢ (((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏)) → 𝜒)

Proof of Theorem ad2ant2r

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantrr 729	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantlr 727	1 ⊢ (((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  disjxiun  5110  fundif  6586  funcnvqp  6601  fliftfun  7311  wfr3g  8315  omordi  8550  nadd4  8684  naddel12  8686  f1imaen2g  9011  isinf  9224  frfi  9244  frr3g  9727  acndom2  10037  infxp  10196  cff1  10241  isf32lem7  10342  fpwwe2lem11  10625  inawinalem  10673  inar1  10759  grur1  10804  genpnnp  10989  ltexprlem7  11026  prlem936  11031  reclem3pr  11033  1re  11207  addsub4  11500  muladd  11645  lt2add  11698  mullt0  11732  mulnzcnf  11859  divmuldiv  11914  divmul24  11918  divmuleq  11919  recdiv  11920  divadddiv  11929  conjmul  11931  prodgt0  12061  ltmul12a  12070  lemul12b  12071  lediv12a  12107  lediv2a  12108  qmulcl  12990  irrmul  12997  xrrege0  13199  xmulge0  13309  ge0addcl  13486  ge0mulcl  13487  ge0xaddcl  13488  ge0xmulcl  13489  fzass4  13589  fzrev  13614  fzocatel  13757  serge0  14091  expclzlem  14118  expge0  14133  expge1  14134  lt2sq  14168  le2sq  14169  bernneq  14264  ccatw2s1p2  14674  swrdccatin2  14765  cshwleneq  14853  s2eq2seq  14973  wwlktovf1  14993  sqrmo  15301  limsupval2  15530  o1lo12  15588  climrlim2  15597  2clim  15622  climsup  15720  tanaddlem  16221  opeo  16422  omeo  16423  divalglem8  16457  coprmproddvdslem  16719  pcpremul  16902  pcmul  16910  setscom  17239  fpwipodrs  18595  gsumsgrpccat  18898  dfgrp3lem  19103  grplactcnv  19108  resgrpisgrp  19213  ghmpreima  19307  ghmeql  19308  conjghm  19318  pgpfi  19674  rngpropd  20251  srhmsubc  20764  lmodprop2d  21022  cndrng  21519  absabv  21542  xrs1mnd  21558  frlmipval  21897  lmimco  21962  mavmulass  22674  mdetdiaglem  22723  cramerimplem2  22809  opnneissb  23239  cncnpi  23403  pnrmopn  23468  cmpsub  23525  connsub  23546  t1connperf  23561  neitx  23732  txcnmpt  23749  txrest  23756  txdis1cn  23760  tx1stc  23775  qtopcn  23839  trfg  24016  rnelfmlem  24077  flffbas  24120  nmo0  24860  nmoid  24867  cfilfcls  25401  iscmet3lem2  25419  caubl  25435  relcmpcmet  25445  ovolun  25626  ovolicc2lem3  25646  volsup  25683  ioombl1lem4  25688  ismbf3d  25781  mbfimaopnlem  25782  i1faddlem  25820  itgle  25937  ellimc2  26004  ftc1a  26164  dgrmul  26395  itgulm  26536  abelthlem8  26567  ptolemy  26626  logdivlt  26751  cxplt3  26830  cxple3  26831  o1cxp  27104  basellem4  27213  sqf11  27268  lgslem3  27428  lgsdir2  27459  lgsne0  27464  lgsquad3  27516  chpo1ubb  27610  vmadivsumb  27612  rpvmasumlem  27616  dchrisum0re  27642  dchrisum0  27649  selberg2b  27681  selberg3lem2  27687  pntrsumbnd  27695  pntrlog2bnd  27713  nocvxmin  27913  mulsgt0  28302  nnaddscl  28504  nnmulscl  28505  ishpg  28999  axcontlem2  29255  umgr2edg  29499  umgrvad2edg  29503  uhgrspan1  29593  wlkeq  29923  clwwlkccatlem  30280  wwlksext2clwwlk  30348  conngrv2edg  30486  frgrnbnb  30584  frgrwopreglem5lem  30611  frgrwopreglem5ALT  30613  grporcan  30810  blocni  31097  ubthlem3  31164  htthlem  31209  hvsub4  31329  shscli  31609  elspansn4  31865  5oalem2  31947  hosub4  32105  hmops  32312  hmopco  32315  adjadd  32385  hstpyth  32521  hstles  32523  mdsl0  32602  mdslmd1lem2  32618  chirredlem1  32682  chirredlem2  32683  chirredlem3  32684  chirredlem4  32685  mdsymlem6  32700  cdj3lem2b  32729  1stpreimas  32991  irngnzply1  34025  mdetpmtr2  34158  esumpcvgval  34412  signstfvc  34905  noinfepfnregs  35467  satffunlem  35791  nmulprop  36580  mpomulnzcnf  36699  tailfb  36776  isbasisrelowllem1  37888  isbasisrelowllem2  37889  poimirlem14  38172  heicant  38193  mblfinlem4  38198  ismblfin  38199  itg2addnc  38212  ftc1cnnc  38230  filbcmb  38278  prdsbnd  38331  ismtyval  38338  heiborlem8  38356  ghomco  38429  mzpindd  43368  tfsconcatun  43955  oaun3lem1  43992  oaun3lem2  43993  mulltgt0  45633  stoweidlem46  46651  fourierdlem73  46784  cfsetsnfsetf1  47684  iccelpart  48070  bgoldbtbnd  48462  grimco  48542  isubgrgrim  48582  usgrgrtrirex  48603  grlictr  48668  2zrngmmgm  48905  srhmsubcALTV  48978  zlmodzxzsubm  49023  zlmodzxzsub  49024