Theorem ad2ant2r 746

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 716	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantlr 714	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  5163  fundif  6627  funcnvqp  6642  fliftfun  7348  wfr3g  8363  omordi  8622  nadd4  8754  naddel12  8756  f1imaen2g  9075  isinf  9323  isinfOLD  9324  frfi  9349  frr3g  9825  acndom2  10123  infxp  10283  cff1  10327  isf32lem7  10428  fpwwe2lem11  10710  inawinalem  10758  inar1  10844  grur1  10889  genpnnp  11074  ltexprlem7  11111  prlem936  11116  reclem3pr  11118  1re  11290  addsub4  11579  muladd  11722  lt2add  11775  mullt0  11809  mulnzcnf  11936  divmuldiv  11994  divmul24  11998  divmuleq  11999  recdiv  12000  divadddiv  12009  conjmul  12011  prodgt0  12141  ltmul12a  12150  lemul12b  12151  lediv12a  12188  lediv2a  12189  qmulcl  13032  irrmul  13039  xrrege0  13236  xmulge0  13346  ge0addcl  13520  ge0mulcl  13521  ge0xaddcl  13522  ge0xmulcl  13523  fzass4  13622  fzrev  13647  fzocatel  13780  serge0  14107  expclzlem  14134  expge0  14149  expge1  14150  lt2sq  14183  le2sq  14184  bernneq  14278  ccatw2s1p2  14685  swrdccatin2  14777  cshwleneq  14865  s2eq2seq  14986  wwlktovf1  15006  sqrmo  15300  limsupval2  15526  o1lo12  15584  climrlim2  15593  2clim  15618  climsup  15718  tanaddlem  16214  opeo  16413  omeo  16414  divalglem8  16448  coprmproddvdslem  16709  pcpremul  16890  pcmul  16898  setscom  17227  fpwipodrs  18610  gsumsgrpccat  18875  dfgrp3lem  19078  grplactcnv  19083  resgrpisgrp  19187  ghmpreima  19278  ghmeql  19279  conjghm  19289  pgpfi  19647  rngpropd  20201  srhmsubc  20702  lmodprop2d  20944  cndrng  21434  xrs1mnd  21445  absabv  21465  frlmipval  21822  lmimco  21887  mavmulass  22576  mdetdiaglem  22625  cramerimplem2  22711  opnneissb  23143  cncnpi  23307  pnrmopn  23372  cmpsub  23429  connsub  23450  t1connperf  23465  neitx  23636  txcnmpt  23653  txrest  23660  txdis1cn  23664  tx1stc  23679  qtopcn  23743  trfg  23920  rnelfmlem  23981  flffbas  24024  nmo0  24777  nmoid  24784  cfilfcls  25327  iscmet3lem2  25345  caubl  25361  relcmpcmet  25371  ovolun  25553  ovolicc2lem3  25573  volsup  25610  ioombl1lem4  25615  ismbf3d  25708  mbfimaopnlem  25709  i1faddlem  25747  itgle  25865  ellimc2  25932  ftc1a  26098  dgrmul  26330  itgulm  26469  abelthlem8  26501  ptolemy  26556  logdivlt  26681  cxplt3  26760  cxple3  26761  o1cxp  27036  basellem4  27145  sqf11  27200  lgslem3  27361  lgsdir2  27392  lgsne0  27397  lgsquad3  27449  chpo1ubb  27543  vmadivsumb  27545  rpvmasumlem  27549  dchrisum0re  27575  dchrisum0  27582  selberg2b  27614  selberg3lem2  27620  pntrsumbnd  27628  pntrlog2bnd  27646  nocvxmin  27841  mulsgt0  28188  nnaddscl  28367  nnmulscl  28368  ishpg  28785  axcontlem2  28998  umgr2edg  29244  umgrvad2edg  29248  uhgrspan1  29338  wlkeq  29670  clwwlkccatlem  30021  wwlksext2clwwlk  30089  conngrv2edg  30227  frgrnbnb  30325  frgrwopreglem5lem  30352  frgrwopreglem5ALT  30354  grporcan  30550  blocni  30837  ubthlem3  30904  htthlem  30949  hvsub4  31069  shscli  31349  elspansn4  31605  5oalem2  31687  hosub4  31845  hmops  32052  hmopco  32055  adjadd  32125  hstpyth  32261  hstles  32263  mdsl0  32342  mdslmd1lem2  32358  chirredlem1  32422  chirredlem2  32423  chirredlem3  32424  chirredlem4  32425  mdsymlem6  32440  cdj3lem2b  32469  1stpreimas  32717  irngnzply1  33691  mdetpmtr2  33770  esumpcvgval  34042  signstfvc  34551  satffunlem  35369  mpomulnzcnf  36265  tailfb  36343  isbasisrelowllem1  37321  isbasisrelowllem2  37322  poimirlem14  37594  heicant  37615  mblfinlem4  37620  ismblfin  37621  itg2addnc  37634  ftc1cnnc  37652  filbcmb  37700  prdsbnd  37753  ismtyval  37760  heiborlem8  37778  ghomco  37851  mzpindd  42702  tfsconcatun  43299  oaun3lem1  43336  oaun3lem2  43337  mulltgt0  44922  stoweidlem46  45967  fourierdlem73  46100  cfsetsnfsetf1  46974  iccelpart  47307  bgoldbtbnd  47683  grimco  47764  isubgrgrim  47781  usgrgrtrirex  47799  grlictr  47832  2zrngmmgm  47975  srhmsubcALTV  48048  zlmodzxzsubm  48084  zlmodzxzsub  48085