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  5089  fundif  6531  funcnvqp  6546  fliftfun  7249  wfr3g  8252  omordi  8484  nadd4  8616  naddel12  8618  f1imaen2g  8940  isinf  9154  frfi  9174  frr3g  9652  acndom2  9948  infxp  10108  cff1  10152  isf32lem7  10253  fpwwe2lem11  10535  inawinalem  10583  inar1  10669  grur1  10714  genpnnp  10899  ltexprlem7  10936  prlem936  10941  reclem3pr  10943  1re  11115  addsub4  11407  muladd  11552  lt2add  11605  mullt0  11639  mulnzcnf  11766  divmuldiv  11824  divmul24  11828  divmuleq  11829  recdiv  11830  divadddiv  11839  conjmul  11841  prodgt0  11971  ltmul12a  11980  lemul12b  11981  lediv12a  12018  lediv2a  12019  qmulcl  12868  irrmul  12875  xrrege0  13076  xmulge0  13186  ge0addcl  13363  ge0mulcl  13364  ge0xaddcl  13365  ge0xmulcl  13366  fzass4  13465  fzrev  13490  fzocatel  13632  serge0  13963  expclzlem  13990  expge0  14005  expge1  14006  lt2sq  14040  le2sq  14041  bernneq  14136  ccatw2s1p2  14544  swrdccatin2  14635  cshwleneq  14723  s2eq2seq  14844  wwlktovf1  14864  sqrmo  15158  limsupval2  15387  o1lo12  15445  climrlim2  15454  2clim  15479  climsup  15577  tanaddlem  16075  opeo  16276  omeo  16277  divalglem8  16311  coprmproddvdslem  16573  pcpremul  16755  pcmul  16763  setscom  17091  fpwipodrs  18446  gsumsgrpccat  18714  dfgrp3lem  18917  grplactcnv  18922  resgrpisgrp  19026  ghmpreima  19117  ghmeql  19118  conjghm  19128  pgpfi  19484  rngpropd  20059  srhmsubc  20565  lmodprop2d  20827  cndrng  21305  absabv  21331  xrs1mnd  21347  frlmipval  21686  lmimco  21751  mavmulass  22434  mdetdiaglem  22483  cramerimplem2  22569  opnneissb  22999  cncnpi  23163  pnrmopn  23228  cmpsub  23285  connsub  23306  t1connperf  23321  neitx  23492  txcnmpt  23509  txrest  23516  txdis1cn  23520  tx1stc  23535  qtopcn  23599  trfg  23776  rnelfmlem  23837  flffbas  23880  nmo0  24621  nmoid  24628  cfilfcls  25172  iscmet3lem2  25190  caubl  25206  relcmpcmet  25216  ovolun  25398  ovolicc2lem3  25418  volsup  25455  ioombl1lem4  25460  ismbf3d  25553  mbfimaopnlem  25554  i1faddlem  25592  itgle  25709  ellimc2  25776  ftc1a  25942  dgrmul  26174  itgulm  26315  abelthlem8  26347  ptolemy  26403  logdivlt  26528  cxplt3  26607  cxple3  26608  o1cxp  26883  basellem4  26992  sqf11  27047  lgslem3  27208  lgsdir2  27239  lgsne0  27244  lgsquad3  27296  chpo1ubb  27390  vmadivsumb  27392  rpvmasumlem  27396  dchrisum0re  27422  dchrisum0  27429  selberg2b  27461  selberg3lem2  27467  pntrsumbnd  27475  pntrlog2bnd  27493  nocvxmin  27689  mulsgt0  28052  nnaddscl  28243  nnmulscl  28244  ishpg  28704  axcontlem2  28910  umgr2edg  29154  umgrvad2edg  29158  uhgrspan1  29248  wlkeq  29579  clwwlkccatlem  29933  wwlksext2clwwlk  30001  conngrv2edg  30139  frgrnbnb  30237  frgrwopreglem5lem  30264  frgrwopreglem5ALT  30266  grporcan  30462  blocni  30749  ubthlem3  30816  htthlem  30861  hvsub4  30981  shscli  31261  elspansn4  31517  5oalem2  31599  hosub4  31757  hmops  31964  hmopco  31967  adjadd  32037  hstpyth  32173  hstles  32175  mdsl0  32254  mdslmd1lem2  32270  chirredlem1  32334  chirredlem2  32335  chirredlem3  32336  chirredlem4  32337  mdsymlem6  32352  cdj3lem2b  32381  1stpreimas  32648  irngnzply1  33658  mdetpmtr2  33791  esumpcvgval  34045  signstfvc  34542  satffunlem  35378  mpomulnzcnf  36277  tailfb  36355  isbasisrelowllem1  37333  isbasisrelowllem2  37334  poimirlem14  37618  heicant  37639  mblfinlem4  37644  ismblfin  37645  itg2addnc  37658  ftc1cnnc  37676  filbcmb  37724  prdsbnd  37777  ismtyval  37784  heiborlem8  37802  ghomco  37875  mzpindd  42723  tfsconcatun  43314  oaun3lem1  43351  oaun3lem2  43352  mulltgt0  45004  stoweidlem46  46031  fourierdlem73  46164  cfsetsnfsetf1  47047  iccelpart  47421  bgoldbtbnd  47797  grimco  47877  isubgrgrim  47917  usgrgrtrirex  47938  grlictr  48003  2zrngmmgm  48240  srhmsubcALTV  48313  zlmodzxzsubm  48347  zlmodzxzsub  48348