Theorem ad2ant2r 748

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 718	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantlr 716	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  5097  fundif  6549  funcnvqp  6564  fliftfun  7268  wfr3g  8271  omordi  8503  nadd4  8636  naddel12  8638  f1imaen2g  8964  isinf  9177  frfi  9197  frr3g  9680  acndom2  9976  infxp  10136  cff1  10180  isf32lem7  10281  fpwwe2lem11  10564  inawinalem  10612  inar1  10698  grur1  10743  genpnnp  10928  ltexprlem7  10965  prlem936  10970  reclem3pr  10972  1re  11144  addsub4  11436  muladd  11581  lt2add  11634  mullt0  11668  mulnzcnf  11795  divmuldiv  11853  divmul24  11857  divmuleq  11858  recdiv  11859  divadddiv  11868  conjmul  11870  prodgt0  12000  ltmul12a  12009  lemul12b  12010  lediv12a  12047  lediv2a  12048  qmulcl  12892  irrmul  12899  xrrege0  13101  xmulge0  13211  ge0addcl  13388  ge0mulcl  13389  ge0xaddcl  13390  ge0xmulcl  13391  fzass4  13490  fzrev  13515  fzocatel  13657  serge0  13991  expclzlem  14018  expge0  14033  expge1  14034  lt2sq  14068  le2sq  14069  bernneq  14164  ccatw2s1p2  14573  swrdccatin2  14664  cshwleneq  14752  s2eq2seq  14872  wwlktovf1  14892  sqrmo  15186  limsupval2  15415  o1lo12  15473  climrlim2  15482  2clim  15507  climsup  15605  tanaddlem  16103  opeo  16304  omeo  16305  divalglem8  16339  coprmproddvdslem  16601  pcpremul  16783  pcmul  16791  setscom  17119  fpwipodrs  18475  gsumsgrpccat  18777  dfgrp3lem  18980  grplactcnv  18985  resgrpisgrp  19089  ghmpreima  19179  ghmeql  19180  conjghm  19190  pgpfi  19546  rngpropd  20121  srhmsubc  20625  lmodprop2d  20887  cndrng  21365  absabv  21391  xrs1mnd  21407  frlmipval  21746  lmimco  21811  mavmulass  22505  mdetdiaglem  22554  cramerimplem2  22640  opnneissb  23070  cncnpi  23234  pnrmopn  23299  cmpsub  23356  connsub  23377  t1connperf  23392  neitx  23563  txcnmpt  23580  txrest  23587  txdis1cn  23591  tx1stc  23606  qtopcn  23670  trfg  23847  rnelfmlem  23908  flffbas  23951  nmo0  24691  nmoid  24698  cfilfcls  25242  iscmet3lem2  25260  caubl  25276  relcmpcmet  25286  ovolun  25468  ovolicc2lem3  25488  volsup  25525  ioombl1lem4  25530  ismbf3d  25623  mbfimaopnlem  25624  i1faddlem  25662  itgle  25779  ellimc2  25846  ftc1a  26012  dgrmul  26244  itgulm  26385  abelthlem8  26417  ptolemy  26473  logdivlt  26598  cxplt3  26677  cxple3  26678  o1cxp  26953  basellem4  27062  sqf11  27117  lgslem3  27278  lgsdir2  27309  lgsne0  27314  lgsquad3  27366  chpo1ubb  27460  vmadivsumb  27462  rpvmasumlem  27466  dchrisum0re  27492  dchrisum0  27499  selberg2b  27531  selberg3lem2  27537  pntrsumbnd  27545  pntrlog2bnd  27563  nocvxmin  27763  mulsgt0  28152  nnaddscl  28354  nnmulscl  28355  ishpg  28843  axcontlem2  29050  umgr2edg  29294  umgrvad2edg  29298  uhgrspan1  29388  wlkeq  29719  clwwlkccatlem  30076  wwlksext2clwwlk  30144  conngrv2edg  30282  frgrnbnb  30380  frgrwopreglem5lem  30407  frgrwopreglem5ALT  30409  grporcan  30606  blocni  30893  ubthlem3  30960  htthlem  31005  hvsub4  31125  shscli  31405  elspansn4  31661  5oalem2  31743  hosub4  31901  hmops  32108  hmopco  32111  adjadd  32181  hstpyth  32317  hstles  32319  mdsl0  32398  mdslmd1lem2  32414  chirredlem1  32478  chirredlem2  32479  chirredlem3  32480  chirredlem4  32481  mdsymlem6  32496  cdj3lem2b  32525  1stpreimas  32796  irngnzply1  33869  mdetpmtr2  34002  esumpcvgval  34256  signstfvc  34752  noinfepfnregs  35310  satffunlem  35617  mpomulnzcnf  36515  tailfb  36593  isbasisrelowllem1  37610  isbasisrelowllem2  37611  poimirlem14  37885  heicant  37906  mblfinlem4  37911  ismblfin  37912  itg2addnc  37925  ftc1cnnc  37943  filbcmb  37991  prdsbnd  38044  ismtyval  38051  heiborlem8  38069  ghomco  38142  mzpindd  43103  tfsconcatun  43694  oaun3lem1  43731  oaun3lem2  43732  mulltgt0  45382  stoweidlem46  46404  fourierdlem73  46537  cfsetsnfsetf1  47419  iccelpart  47793  bgoldbtbnd  48169  grimco  48249  isubgrgrim  48289  usgrgrtrirex  48310  grlictr  48375  2zrngmmgm  48612  srhmsubcALTV  48685  zlmodzxzsubm  48719  zlmodzxzsub  48720