Theorem ad2ant2r 745

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 715	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantlr 713	1 ⊢ (((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  disjxiun  5100  fundif  6545  funcnvqp  6560  fliftfun  7251  wfr3g  8220  omordi  8480  f1imaen2g  8888  isinf  9137  isinfOLD  9138  frfi  9165  frr3g  9625  acndom2  9923  infxp  10084  cff1  10127  isf32lem7  10228  fpwwe2lem11  10510  inawinalem  10558  inar1  10644  grur1  10689  genpnnp  10874  ltexprlem7  10911  prlem936  10916  reclem3pr  10918  1re  11088  addsub4  11377  muladd  11520  lt2add  11573  mullt0  11607  mulnzcnopr  11734  divmuldiv  11788  divmul24  11792  divmuleq  11793  recdiv  11794  divadddiv  11803  conjmul  11805  prodgt0  11935  ltmul12a  11944  lemul12b  11945  lediv12a  11981  lediv2a  11982  qmulcl  12820  irrmul  12827  xrrege0  13021  xmulge0  13131  ge0addcl  13305  ge0mulcl  13306  ge0xaddcl  13307  ge0xmulcl  13308  fzass4  13407  fzrev  13432  fzocatel  13564  serge0  13890  expclzlem  13919  expge0  13932  expge1  13933  lt2sq  13965  le2sq  13966  bernneq  14057  ccatw2s1p1OLD  14453  ccatw2s1p2  14454  swrdccatin2  14548  cshwleneq  14636  s2eq2seq  14757  wwlktovf1  14779  sqrmo  15070  limsupval2  15296  o1lo12  15354  climrlim2  15363  2clim  15388  climsup  15488  tanaddlem  15982  opeo  16181  omeo  16182  divalglem8  16216  coprmproddvdslem  16472  pcpremul  16649  pcmul  16657  setscom  16986  fpwipodrs  18363  gsumsgrpccat  18583  dfgrp3lem  18777  grplactcnv  18782  resgrpisgrp  18880  ghmpreima  18960  ghmeql  18961  conjghm  18969  pgpfi  19314  lmodprop2d  20298  lidlmcl  20601  xrs1mnd  20749  absabv  20768  frlmipval  21099  lmimco  21164  mavmulass  21811  mdetdiaglem  21860  cramerimplem2  21946  opnneissb  22378  cncnpi  22542  pnrmopn  22607  cmpsub  22664  connsub  22685  t1connperf  22700  neitx  22871  txcnmpt  22888  txrest  22895  txdis1cn  22899  tx1stc  22914  qtopcn  22978  trfg  23155  rnelfmlem  23216  flffbas  23259  nmo0  24012  nmoid  24019  cfilfcls  24551  iscmet3lem2  24569  caubl  24585  relcmpcmet  24595  ovolun  24776  ovolicc2lem3  24796  volsup  24833  ioombl1lem4  24838  ismbf3d  24931  mbfimaopnlem  24932  i1faddlem  24970  itgle  25087  ellimc2  25154  ftc1a  25314  dgrmul  25544  itgulm  25680  abelthlem8  25711  ptolemy  25766  logdivlt  25889  cxplt3  25968  cxple3  25969  o1cxp  26237  basellem4  26346  sqf11  26401  lgslem3  26560  lgsdir2  26591  lgsne0  26596  lgsquad3  26648  chpo1ubb  26742  vmadivsumb  26744  rpvmasumlem  26748  dchrisum0re  26774  dchrisum0  26781  selberg2b  26813  selberg3lem2  26819  pntrsumbnd  26827  pntrlog2bnd  26845  nocvxmin  27031  ishpg  27478  axcontlem2  27691  umgr2edg  27934  umgrvad2edg  27938  uhgrspan1  28028  wlkeq  28359  clwwlkccatlem  28710  wwlksext2clwwlk  28778  conngrv2edg  28916  frgrnbnb  29014  frgrwopreglem5lem  29041  frgrwopreglem5ALT  29043  grporcan  29237  blocni  29524  ubthlem3  29591  htthlem  29636  hvsub4  29756  shscli  30036  elspansn4  30292  5oalem2  30374  hosub4  30532  hmops  30739  hmopco  30742  adjadd  30812  hstpyth  30948  hstles  30950  mdsl0  31029  mdslmd1lem2  31045  chirredlem1  31109  chirredlem2  31110  chirredlem3  31111  chirredlem4  31112  mdsymlem6  31127  cdj3lem2b  31156  1stpreimas  31392  mdetpmtr2  32139  esumpcvgval  32411  signstfvc  32920  satffunlem  33729  tailfb  34708  isbasisrelowllem1  35685  isbasisrelowllem2  35686  poimirlem14  35951  heicant  35972  mblfinlem4  35977  ismblfin  35978  itg2addnc  35991  ftc1cnnc  36009  filbcmb  36058  prdsbnd  36111  ismtyval  36118  heiborlem8  36136  ghomco  36209  mzpindd  40885  mulltgt0  42942  stoweidlem46  43979  fourierdlem73  44112  cfsetsnfsetf1  44975  iccelpart  45307  bgoldbtbnd  45683  2zrngmmgm  45926  srhmsubc  46056  srhmsubcALTV  46074  zlmodzxzsubm  46117  zlmodzxzsub  46118