Theorem ad2ant2r 747

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 717	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantlr 715	1 ⊢ (((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  disjxiun  5144  fundif  6616  funcnvqp  6631  fliftfun  7331  wfr3g  8345  omordi  8602  nadd4  8734  naddel12  8736  f1imaen2g  9053  isinf  9293  isinfOLD  9294  frfi  9318  frr3g  9793  acndom2  10091  infxp  10251  cff1  10295  isf32lem7  10396  fpwwe2lem11  10678  inawinalem  10726  inar1  10812  grur1  10857  genpnnp  11042  ltexprlem7  11079  prlem936  11084  reclem3pr  11086  1re  11258  addsub4  11549  muladd  11692  lt2add  11745  mullt0  11779  mulnzcnf  11906  divmuldiv  11964  divmul24  11968  divmuleq  11969  recdiv  11970  divadddiv  11979  conjmul  11981  prodgt0  12111  ltmul12a  12120  lemul12b  12121  lediv12a  12158  lediv2a  12159  qmulcl  13006  irrmul  13013  xrrege0  13212  xmulge0  13322  ge0addcl  13496  ge0mulcl  13497  ge0xaddcl  13498  ge0xmulcl  13499  fzass4  13598  fzrev  13623  fzocatel  13764  serge0  14093  expclzlem  14120  expge0  14135  expge1  14136  lt2sq  14169  le2sq  14170  bernneq  14264  ccatw2s1p2  14671  swrdccatin2  14763  cshwleneq  14851  s2eq2seq  14972  wwlktovf1  14992  sqrmo  15286  limsupval2  15512  o1lo12  15570  climrlim2  15579  2clim  15604  climsup  15702  tanaddlem  16198  opeo  16398  omeo  16399  divalglem8  16433  coprmproddvdslem  16695  pcpremul  16876  pcmul  16884  setscom  17213  fpwipodrs  18597  gsumsgrpccat  18865  dfgrp3lem  19068  grplactcnv  19073  resgrpisgrp  19177  ghmpreima  19268  ghmeql  19269  conjghm  19279  pgpfi  19637  rngpropd  20191  srhmsubc  20696  lmodprop2d  20938  cndrng  21428  xrs1mnd  21439  absabv  21459  frlmipval  21816  lmimco  21881  mavmulass  22570  mdetdiaglem  22619  cramerimplem2  22705  opnneissb  23137  cncnpi  23301  pnrmopn  23366  cmpsub  23423  connsub  23444  t1connperf  23459  neitx  23630  txcnmpt  23647  txrest  23654  txdis1cn  23658  tx1stc  23673  qtopcn  23737  trfg  23914  rnelfmlem  23975  flffbas  24018  nmo0  24771  nmoid  24778  cfilfcls  25321  iscmet3lem2  25339  caubl  25355  relcmpcmet  25365  ovolun  25547  ovolicc2lem3  25567  volsup  25604  ioombl1lem4  25609  ismbf3d  25702  mbfimaopnlem  25703  i1faddlem  25741  itgle  25859  ellimc2  25926  ftc1a  26092  dgrmul  26324  itgulm  26465  abelthlem8  26497  ptolemy  26552  logdivlt  26677  cxplt3  26756  cxple3  26757  o1cxp  27032  basellem4  27141  sqf11  27196  lgslem3  27357  lgsdir2  27388  lgsne0  27393  lgsquad3  27445  chpo1ubb  27539  vmadivsumb  27541  rpvmasumlem  27545  dchrisum0re  27571  dchrisum0  27578  selberg2b  27610  selberg3lem2  27616  pntrsumbnd  27624  pntrlog2bnd  27642  nocvxmin  27837  mulsgt0  28184  nnaddscl  28363  nnmulscl  28364  ishpg  28781  axcontlem2  28994  umgr2edg  29240  umgrvad2edg  29244  uhgrspan1  29334  wlkeq  29666  clwwlkccatlem  30017  wwlksext2clwwlk  30085  conngrv2edg  30223  frgrnbnb  30321  frgrwopreglem5lem  30348  frgrwopreglem5ALT  30350  grporcan  30546  blocni  30833  ubthlem3  30900  htthlem  30945  hvsub4  31065  shscli  31345  elspansn4  31601  5oalem2  31683  hosub4  31841  hmops  32048  hmopco  32051  adjadd  32121  hstpyth  32257  hstles  32259  mdsl0  32338  mdslmd1lem2  32354  chirredlem1  32418  chirredlem2  32419  chirredlem3  32420  chirredlem4  32421  mdsymlem6  32436  cdj3lem2b  32465  1stpreimas  32720  irngnzply1  33705  mdetpmtr2  33784  esumpcvgval  34058  signstfvc  34567  satffunlem  35385  mpomulnzcnf  36281  tailfb  36359  isbasisrelowllem1  37337  isbasisrelowllem2  37338  poimirlem14  37620  heicant  37641  mblfinlem4  37646  ismblfin  37647  itg2addnc  37660  ftc1cnnc  37678  filbcmb  37726  prdsbnd  37779  ismtyval  37786  heiborlem8  37804  ghomco  37877  mzpindd  42733  tfsconcatun  43326  oaun3lem1  43363  oaun3lem2  43364  mulltgt0  44959  stoweidlem46  46001  fourierdlem73  46134  cfsetsnfsetf1  47008  iccelpart  47357  bgoldbtbnd  47733  grimco  47817  isubgrgrim  47834  usgrgrtrirex  47852  grlictr  47910  2zrngmmgm  48095  srhmsubcALTV  48168  zlmodzxzsubm  48203  zlmodzxzsub  48204