Theorem ad2ant2r 779

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  disjxiun  4579  fundif  5849  funcnvqp  5866  foco  6038  fliftfun  6462  wfr3g  7300  omordi  7533  f1imaen2g  7903  isinf  8058  frfi  8090  acndom2  8760  infxp  8920  cff1  8963  isf32lem7  9064  fpwwe2lem12  9342  inawinalem  9390  inar1  9476  grur1  9521  genpnnp  9706  ltexprlem7  9743  prlem936  9748  reclem3pr  9750  1re  9918  addsub4  10203  muladd  10341  lt2add  10392  mullt0  10426  mulnzcnopr  10552  divmuldiv  10604  divmul24  10608  divmuleq  10609  recdiv  10610  divadddiv  10619  conjmul  10621  prodgt0  10747  ltmul12a  10758  lemul12b  10759  lediv12a  10795  lediv2a  10796  qmulcl  11682  irrmul  11689  xrrege0  11879  xmulge0  11986  ge0addcl  12155  ge0mulcl  12156  ge0xaddcl  12157  ge0xmulcl  12158  fzass4  12250  fzrev  12273  fzocatel  12399  serge0  12717  expclzlem  12746  expge0  12758  expge1  12759  lt2sq  12799  le2sq  12800  bernneq  12852  ccatw2s1p1  13265  ccatw2s1p2  13266  cshwleneq  13414  s2eq2seq  13532  sqrmo  13840  limsupval2  14059  o1lo12  14117  climrlim2  14126  2clim  14151  climsup  14248  tanaddlem  14735  opeo  14927  omeo  14928  divalglem8  14961  coprmproddvdslem  15214  pcpremul  15386  pcmul  15394  setscom  15731  fpwipodrs  16987  dfgrp3lem  17336  grplactcnv  17341  resgrpisgrp  17438  ghmpreima  17505  ghmeql  17506  conjghm  17514  pgpfi  17843  lmodprop2d  18748  lidlmcl  19038  xrs1mnd  19603  absabv  19622  frlmipval  19937  lmimco  20002  mavmulass  20174  mdetdiaglem  20223  cramerimplem2  20309  opnneissb  20728  cncnpi  20892  pnrmopn  20957  cmpsub  21013  connsub  21034  t1conperf  21049  neitx  21220  txcnmpt  21237  txrest  21244  txdis1cn  21248  tx1stc  21263  qtopcn  21327  trfg  21505  rnelfmlem  21566  flffbas  21609  nmo0  22349  nmoid  22356  cfilfcls  22880  iscmet3lem2  22898  caubl  22914  relcmpcmet  22923  ovolun  23074  ovolicc2lem3  23094  volsup  23131  ioombl1lem4  23136  ismbf3d  23227  mbfimaopnlem  23228  i1faddlem  23266  itgle  23382  ellimc2  23447  ftc1a  23604  dgrmul  23830  itgulm  23966  abelthlem8  23997  ptolemy  24052  logdivlt  24171  cxplt3  24246  cxple3  24247  o1cxp  24501  basellem4  24610  sqf11  24665  lgslem3  24824  lgsdir2  24855  lgsne0  24860  lgsquad3  24912  chpo1ubb  24970  vmadivsumb  24972  rpvmasumlem  24976  dchrisum0re  25002  dchrisum0  25009  selberg2b  25041  selberg3lem2  25047  pntrsumbnd  25055  pntrlog2bnd  25073  axcontlem2  25645  usgra2adedgspth  26141  2wlkeq  26235  wwlkext2clwwlk  26331  grporcan  26756  blocni  27044  ubthlem3  27112  htthlem  27158  hvsub4  27278  shscli  27560  elspansn4  27816  5oalem2  27898  hosub4  28056  hmops  28263  hmopco  28266  adjadd  28336  hstpyth  28472  hstles  28474  mdsl0  28553  mdslmd1lem2  28569  chirredlem1  28633  chirredlem2  28634  chirredlem3  28635  chirredlem4  28636  mdsymlem6  28651  cdj3lem2b  28680  1stpreimas  28866  mdetpmtr2  29218  esumpcvgval  29467  frr3g  31023  nocvxmin  31090  tailfb  31542  isbasisrelowllem1  32379  isbasisrelowllem2  32380  poimirlem14  32593  heicant  32614  mblfinlem4  32619  ismblfin  32620  itg2addnc  32634  ftc1cnnc  32654  filbcmb  32705  prdsbnd  32762  ismtyval  32769  heiborlem8  32787  ghomco  32860  mzpindd  36327  rp-fakenanass  36879  mulltgt0  38204  stoweidlem46  38939  fourierdlem73  39072  iccelpart  39971  bgoldbtbnd  40225  umgr2edg  40436  umgrvad2edg  40440  uhgrspan1  40527  1wlkeq  40838  wwlksext2clwwlk  41231  conngrv2edg  41362  frgrnbnb  41463  2zrngmmgm  41736  srhmsubc  41868  srhmsubcALTV  41887  zlmodzxzsubm  41930  zlmodzxzsub  41931