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  5140  fundif  6615  funcnvqp  6630  fliftfun  7332  wfr3g  8347  omordi  8604  nadd4  8736  naddel12  8738  f1imaen2g  9055  isinf  9296  isinfOLD  9297  frfi  9321  frr3g  9796  acndom2  10094  infxp  10254  cff1  10298  isf32lem7  10399  fpwwe2lem11  10681  inawinalem  10729  inar1  10815  grur1  10860  genpnnp  11045  ltexprlem7  11082  prlem936  11087  reclem3pr  11089  1re  11261  addsub4  11552  muladd  11695  lt2add  11748  mullt0  11782  mulnzcnf  11909  divmuldiv  11967  divmul24  11971  divmuleq  11972  recdiv  11973  divadddiv  11982  conjmul  11984  prodgt0  12114  ltmul12a  12123  lemul12b  12124  lediv12a  12161  lediv2a  12162  qmulcl  13009  irrmul  13016  xrrege0  13216  xmulge0  13326  ge0addcl  13500  ge0mulcl  13501  ge0xaddcl  13502  ge0xmulcl  13503  fzass4  13602  fzrev  13627  fzocatel  13768  serge0  14097  expclzlem  14124  expge0  14139  expge1  14140  lt2sq  14173  le2sq  14174  bernneq  14268  ccatw2s1p2  14675  swrdccatin2  14767  cshwleneq  14855  s2eq2seq  14976  wwlktovf1  14996  sqrmo  15290  limsupval2  15516  o1lo12  15574  climrlim2  15583  2clim  15608  climsup  15706  tanaddlem  16202  opeo  16402  omeo  16403  divalglem8  16437  coprmproddvdslem  16699  pcpremul  16881  pcmul  16889  setscom  17217  fpwipodrs  18585  gsumsgrpccat  18853  dfgrp3lem  19056  grplactcnv  19061  resgrpisgrp  19165  ghmpreima  19256  ghmeql  19257  conjghm  19267  pgpfi  19623  rngpropd  20171  srhmsubc  20680  lmodprop2d  20922  cndrng  21411  xrs1mnd  21422  absabv  21442  frlmipval  21799  lmimco  21864  mavmulass  22555  mdetdiaglem  22604  cramerimplem2  22690  opnneissb  23122  cncnpi  23286  pnrmopn  23351  cmpsub  23408  connsub  23429  t1connperf  23444  neitx  23615  txcnmpt  23632  txrest  23639  txdis1cn  23643  tx1stc  23658  qtopcn  23722  trfg  23899  rnelfmlem  23960  flffbas  24003  nmo0  24756  nmoid  24763  cfilfcls  25308  iscmet3lem2  25326  caubl  25342  relcmpcmet  25352  ovolun  25534  ovolicc2lem3  25554  volsup  25591  ioombl1lem4  25596  ismbf3d  25689  mbfimaopnlem  25690  i1faddlem  25728  itgle  25845  ellimc2  25912  ftc1a  26078  dgrmul  26310  itgulm  26451  abelthlem8  26483  ptolemy  26538  logdivlt  26663  cxplt3  26742  cxple3  26743  o1cxp  27018  basellem4  27127  sqf11  27182  lgslem3  27343  lgsdir2  27374  lgsne0  27379  lgsquad3  27431  chpo1ubb  27525  vmadivsumb  27527  rpvmasumlem  27531  dchrisum0re  27557  dchrisum0  27564  selberg2b  27596  selberg3lem2  27602  pntrsumbnd  27610  pntrlog2bnd  27628  nocvxmin  27823  mulsgt0  28170  nnaddscl  28349  nnmulscl  28350  ishpg  28767  axcontlem2  28980  umgr2edg  29226  umgrvad2edg  29230  uhgrspan1  29320  wlkeq  29652  clwwlkccatlem  30008  wwlksext2clwwlk  30076  conngrv2edg  30214  frgrnbnb  30312  frgrwopreglem5lem  30339  frgrwopreglem5ALT  30341  grporcan  30537  blocni  30824  ubthlem3  30891  htthlem  30936  hvsub4  31056  shscli  31336  elspansn4  31592  5oalem2  31674  hosub4  31832  hmops  32039  hmopco  32042  adjadd  32112  hstpyth  32248  hstles  32250  mdsl0  32329  mdslmd1lem2  32345  chirredlem1  32409  chirredlem2  32410  chirredlem3  32411  chirredlem4  32412  mdsymlem6  32427  cdj3lem2b  32456  1stpreimas  32715  irngnzply1  33741  mdetpmtr2  33823  esumpcvgval  34079  signstfvc  34589  satffunlem  35406  mpomulnzcnf  36300  tailfb  36378  isbasisrelowllem1  37356  isbasisrelowllem2  37357  poimirlem14  37641  heicant  37662  mblfinlem4  37667  ismblfin  37668  itg2addnc  37681  ftc1cnnc  37699  filbcmb  37747  prdsbnd  37800  ismtyval  37807  heiborlem8  37825  ghomco  37898  mzpindd  42757  tfsconcatun  43350  oaun3lem1  43387  oaun3lem2  43388  mulltgt0  45027  stoweidlem46  46061  fourierdlem73  46194  cfsetsnfsetf1  47071  iccelpart  47420  bgoldbtbnd  47796  grimco  47880  isubgrgrim  47897  usgrgrtrirex  47917  grlictr  47975  2zrngmmgm  48168  srhmsubcALTV  48241  zlmodzxzsubm  48275  zlmodzxzsub  48276