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  5093  fundif  6539  funcnvqp  6554  fliftfun  7256  wfr3g  8259  omordi  8491  nadd4  8624  naddel12  8626  f1imaen2g  8950  isinf  9163  frfi  9183  frr3g  9666  acndom2  9962  infxp  10122  cff1  10166  isf32lem7  10267  fpwwe2lem11  10550  inawinalem  10598  inar1  10684  grur1  10729  genpnnp  10914  ltexprlem7  10951  prlem936  10956  reclem3pr  10958  1re  11130  addsub4  11422  muladd  11567  lt2add  11620  mullt0  11654  mulnzcnf  11781  divmuldiv  11839  divmul24  11843  divmuleq  11844  recdiv  11845  divadddiv  11854  conjmul  11856  prodgt0  11986  ltmul12a  11995  lemul12b  11996  lediv12a  12033  lediv2a  12034  qmulcl  12878  irrmul  12885  xrrege0  13087  xmulge0  13197  ge0addcl  13374  ge0mulcl  13375  ge0xaddcl  13376  ge0xmulcl  13377  fzass4  13476  fzrev  13501  fzocatel  13643  serge0  13977  expclzlem  14004  expge0  14019  expge1  14020  lt2sq  14054  le2sq  14055  bernneq  14150  ccatw2s1p2  14559  swrdccatin2  14650  cshwleneq  14738  s2eq2seq  14858  wwlktovf1  14878  sqrmo  15172  limsupval2  15401  o1lo12  15459  climrlim2  15468  2clim  15493  climsup  15591  tanaddlem  16089  opeo  16290  omeo  16291  divalglem8  16325  coprmproddvdslem  16587  pcpremul  16769  pcmul  16777  setscom  17105  fpwipodrs  18461  gsumsgrpccat  18763  dfgrp3lem  18966  grplactcnv  18971  resgrpisgrp  19075  ghmpreima  19165  ghmeql  19166  conjghm  19176  pgpfi  19532  rngpropd  20107  srhmsubc  20611  lmodprop2d  20873  cndrng  21351  absabv  21377  xrs1mnd  21393  frlmipval  21732  lmimco  21797  mavmulass  22491  mdetdiaglem  22540  cramerimplem2  22626  opnneissb  23056  cncnpi  23220  pnrmopn  23285  cmpsub  23342  connsub  23363  t1connperf  23378  neitx  23549  txcnmpt  23566  txrest  23573  txdis1cn  23577  tx1stc  23592  qtopcn  23656  trfg  23833  rnelfmlem  23894  flffbas  23937  nmo0  24677  nmoid  24684  cfilfcls  25228  iscmet3lem2  25246  caubl  25262  relcmpcmet  25272  ovolun  25454  ovolicc2lem3  25474  volsup  25511  ioombl1lem4  25516  ismbf3d  25609  mbfimaopnlem  25610  i1faddlem  25648  itgle  25765  ellimc2  25832  ftc1a  25998  dgrmul  26230  itgulm  26371  abelthlem8  26403  ptolemy  26459  logdivlt  26584  cxplt3  26663  cxple3  26664  o1cxp  26939  basellem4  27048  sqf11  27103  lgslem3  27264  lgsdir2  27295  lgsne0  27300  lgsquad3  27352  chpo1ubb  27446  vmadivsumb  27448  rpvmasumlem  27452  dchrisum0re  27478  dchrisum0  27485  selberg2b  27517  selberg3lem2  27523  pntrsumbnd  27531  pntrlog2bnd  27549  nocvxmin  27745  mulsgt0  28113  nnaddscl  28306  nnmulscl  28307  ishpg  28780  axcontlem2  28987  umgr2edg  29231  umgrvad2edg  29235  uhgrspan1  29325  wlkeq  29656  clwwlkccatlem  30013  wwlksext2clwwlk  30081  conngrv2edg  30219  frgrnbnb  30317  frgrwopreglem5lem  30344  frgrwopreglem5ALT  30346  grporcan  30542  blocni  30829  ubthlem3  30896  htthlem  30941  hvsub4  31061  shscli  31341  elspansn4  31597  5oalem2  31679  hosub4  31837  hmops  32044  hmopco  32047  adjadd  32117  hstpyth  32253  hstles  32255  mdsl0  32334  mdslmd1lem2  32350  chirredlem1  32414  chirredlem2  32415  chirredlem3  32416  chirredlem4  32417  mdsymlem6  32432  cdj3lem2b  32461  1stpreimas  32734  irngnzply1  33797  mdetpmtr2  33930  esumpcvgval  34184  signstfvc  34680  noinfepfnregs  35237  satffunlem  35544  mpomulnzcnf  36442  tailfb  36520  isbasisrelowllem1  37499  isbasisrelowllem2  37500  poimirlem14  37774  heicant  37795  mblfinlem4  37800  ismblfin  37801  itg2addnc  37814  ftc1cnnc  37832  filbcmb  37880  prdsbnd  37933  ismtyval  37940  heiborlem8  37958  ghomco  38031  mzpindd  42930  tfsconcatun  43521  oaun3lem1  43558  oaun3lem2  43559  mulltgt0  45209  stoweidlem46  46232  fourierdlem73  46365  cfsetsnfsetf1  47247  iccelpart  47621  bgoldbtbnd  47997  grimco  48077  isubgrgrim  48117  usgrgrtrirex  48138  grlictr  48203  2zrngmmgm  48440  srhmsubcALTV  48513  zlmodzxzsubm  48547  zlmodzxzsub  48548