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  5086  fundif  6530  funcnvqp  6545  fliftfun  7246  wfr3g  8249  omordi  8481  nadd4  8613  naddel12  8615  f1imaen2g  8937  isinf  9149  frfi  9169  frr3g  9649  acndom2  9945  infxp  10105  cff1  10149  isf32lem7  10250  fpwwe2lem11  10532  inawinalem  10580  inar1  10666  grur1  10711  genpnnp  10896  ltexprlem7  10933  prlem936  10938  reclem3pr  10940  1re  11112  addsub4  11404  muladd  11549  lt2add  11602  mullt0  11636  mulnzcnf  11763  divmuldiv  11821  divmul24  11825  divmuleq  11826  recdiv  11827  divadddiv  11836  conjmul  11838  prodgt0  11968  ltmul12a  11977  lemul12b  11978  lediv12a  12015  lediv2a  12016  qmulcl  12865  irrmul  12872  xrrege0  13073  xmulge0  13183  ge0addcl  13360  ge0mulcl  13361  ge0xaddcl  13362  ge0xmulcl  13363  fzass4  13462  fzrev  13487  fzocatel  13629  serge0  13963  expclzlem  13990  expge0  14005  expge1  14006  lt2sq  14040  le2sq  14041  bernneq  14136  ccatw2s1p2  14545  swrdccatin2  14636  cshwleneq  14724  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  18748  dfgrp3lem  18951  grplactcnv  18956  resgrpisgrp  19060  ghmpreima  19150  ghmeql  19151  conjghm  19161  pgpfi  19517  rngpropd  20092  srhmsubc  20595  lmodprop2d  20857  cndrng  21335  absabv  21361  xrs1mnd  21377  frlmipval  21716  lmimco  21781  mavmulass  22464  mdetdiaglem  22513  cramerimplem2  22599  opnneissb  23029  cncnpi  23193  pnrmopn  23258  cmpsub  23315  connsub  23336  t1connperf  23351  neitx  23522  txcnmpt  23539  txrest  23546  txdis1cn  23550  tx1stc  23565  qtopcn  23629  trfg  23806  rnelfmlem  23867  flffbas  23910  nmo0  24650  nmoid  24657  cfilfcls  25201  iscmet3lem2  25219  caubl  25235  relcmpcmet  25245  ovolun  25427  ovolicc2lem3  25447  volsup  25484  ioombl1lem4  25489  ismbf3d  25582  mbfimaopnlem  25583  i1faddlem  25621  itgle  25738  ellimc2  25805  ftc1a  25971  dgrmul  26203  itgulm  26344  abelthlem8  26376  ptolemy  26432  logdivlt  26557  cxplt3  26636  cxple3  26637  o1cxp  26912  basellem4  27021  sqf11  27076  lgslem3  27237  lgsdir2  27268  lgsne0  27273  lgsquad3  27325  chpo1ubb  27419  vmadivsumb  27421  rpvmasumlem  27425  dchrisum0re  27451  dchrisum0  27458  selberg2b  27490  selberg3lem2  27496  pntrsumbnd  27504  pntrlog2bnd  27522  nocvxmin  27718  mulsgt0  28083  nnaddscl  28274  nnmulscl  28275  ishpg  28737  axcontlem2  28943  umgr2edg  29187  umgrvad2edg  29191  uhgrspan1  29281  wlkeq  29612  clwwlkccatlem  29969  wwlksext2clwwlk  30037  conngrv2edg  30175  frgrnbnb  30273  frgrwopreglem5lem  30300  frgrwopreglem5ALT  30302  grporcan  30498  blocni  30785  ubthlem3  30852  htthlem  30897  hvsub4  31017  shscli  31297  elspansn4  31553  5oalem2  31635  hosub4  31793  hmops  32000  hmopco  32003  adjadd  32073  hstpyth  32209  hstles  32211  mdsl0  32290  mdslmd1lem2  32306  chirredlem1  32370  chirredlem2  32371  chirredlem3  32372  chirredlem4  32373  mdsymlem6  32388  cdj3lem2b  32417  1stpreimas  32687  irngnzply1  33704  mdetpmtr2  33837  esumpcvgval  34091  signstfvc  34587  satffunlem  35445  mpomulnzcnf  36343  tailfb  36421  isbasisrelowllem1  37399  isbasisrelowllem2  37400  poimirlem14  37684  heicant  37705  mblfinlem4  37710  ismblfin  37711  itg2addnc  37724  ftc1cnnc  37742  filbcmb  37790  prdsbnd  37843  ismtyval  37850  heiborlem8  37868  ghomco  37941  mzpindd  42849  tfsconcatun  43440  oaun3lem1  43477  oaun3lem2  43478  mulltgt0  45129  stoweidlem46  46154  fourierdlem73  46287  cfsetsnfsetf1  47169  iccelpart  47543  bgoldbtbnd  47919  grimco  47999  isubgrgrim  48039  usgrgrtrirex  48060  grlictr  48125  2zrngmmgm  48362  srhmsubcALTV  48435  zlmodzxzsubm  48469  zlmodzxzsub  48470