Theorem ad2ant2r 744

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  disjxiun  5071  fundif  6483  funcnvqp  6498  fliftfun  7183  wfr3g  8138  omordi  8397  f1imaen2g  8801  isinf  9036  frfi  9059  frr3g  9514  acndom2  9810  infxp  9971  cff1  10014  isf32lem7  10115  fpwwe2lem11  10397  inawinalem  10445  inar1  10531  grur1  10576  genpnnp  10761  ltexprlem7  10798  prlem936  10803  reclem3pr  10805  1re  10975  addsub4  11264  muladd  11407  lt2add  11460  mullt0  11494  mulnzcnopr  11621  divmuldiv  11675  divmul24  11679  divmuleq  11680  recdiv  11681  divadddiv  11690  conjmul  11692  prodgt0  11822  ltmul12a  11831  lemul12b  11832  lediv12a  11868  lediv2a  11869  qmulcl  12707  irrmul  12714  xrrege0  12908  xmulge0  13018  ge0addcl  13192  ge0mulcl  13193  ge0xaddcl  13194  ge0xmulcl  13195  fzass4  13294  fzrev  13319  fzocatel  13451  serge0  13777  expclzlem  13806  expge0  13819  expge1  13820  lt2sq  13852  le2sq  13853  bernneq  13944  ccatw2s1p1OLD  14347  ccatw2s1p2  14348  swrdccatin2  14442  cshwleneq  14530  s2eq2seq  14650  wwlktovf1  14672  sqrmo  14963  limsupval2  15189  o1lo12  15247  climrlim2  15256  2clim  15281  climsup  15381  tanaddlem  15875  opeo  16074  omeo  16075  divalglem8  16109  coprmproddvdslem  16367  pcpremul  16544  pcmul  16552  setscom  16881  fpwipodrs  18258  gsumsgrpccat  18478  dfgrp3lem  18673  grplactcnv  18678  resgrpisgrp  18776  ghmpreima  18856  ghmeql  18857  conjghm  18865  pgpfi  19210  lmodprop2d  20185  lidlmcl  20488  xrs1mnd  20636  absabv  20655  frlmipval  20986  lmimco  21051  mavmulass  21698  mdetdiaglem  21747  cramerimplem2  21833  opnneissb  22265  cncnpi  22429  pnrmopn  22494  cmpsub  22551  connsub  22572  t1connperf  22587  neitx  22758  txcnmpt  22775  txrest  22782  txdis1cn  22786  tx1stc  22801  qtopcn  22865  trfg  23042  rnelfmlem  23103  flffbas  23146  nmo0  23899  nmoid  23906  cfilfcls  24438  iscmet3lem2  24456  caubl  24472  relcmpcmet  24482  ovolun  24663  ovolicc2lem3  24683  volsup  24720  ioombl1lem4  24725  ismbf3d  24818  mbfimaopnlem  24819  i1faddlem  24857  itgle  24974  ellimc2  25041  ftc1a  25201  dgrmul  25431  itgulm  25567  abelthlem8  25598  ptolemy  25653  logdivlt  25776  cxplt3  25855  cxple3  25856  o1cxp  26124  basellem4  26233  sqf11  26288  lgslem3  26447  lgsdir2  26478  lgsne0  26483  lgsquad3  26535  chpo1ubb  26629  vmadivsumb  26631  rpvmasumlem  26635  dchrisum0re  26661  dchrisum0  26668  selberg2b  26700  selberg3lem2  26706  pntrsumbnd  26714  pntrlog2bnd  26732  ishpg  27120  axcontlem2  27333  umgr2edg  27576  umgrvad2edg  27580  uhgrspan1  27670  wlkeq  28001  clwwlkccatlem  28353  wwlksext2clwwlk  28421  conngrv2edg  28559  frgrnbnb  28657  frgrwopreglem5lem  28684  frgrwopreglem5ALT  28686  grporcan  28880  blocni  29167  ubthlem3  29234  htthlem  29279  hvsub4  29399  shscli  29679  elspansn4  29935  5oalem2  30017  hosub4  30175  hmops  30382  hmopco  30385  adjadd  30455  hstpyth  30591  hstles  30593  mdsl0  30672  mdslmd1lem2  30688  chirredlem1  30752  chirredlem2  30753  chirredlem3  30754  chirredlem4  30755  mdsymlem6  30770  cdj3lem2b  30799  1stpreimas  31038  mdetpmtr2  31774  esumpcvgval  32046  signstfvc  32553  satffunlem  33363  nocvxmin  33973  tailfb  34566  isbasisrelowllem1  35526  isbasisrelowllem2  35527  poimirlem14  35791  heicant  35812  mblfinlem4  35817  ismblfin  35818  itg2addnc  35831  ftc1cnnc  35849  filbcmb  35898  prdsbnd  35951  ismtyval  35958  heiborlem8  35976  ghomco  36049  mzpindd  40568  mulltgt0  42565  stoweidlem46  43587  fourierdlem73  43720  cfsetsnfsetf1  44553  iccelpart  44885  bgoldbtbnd  45261  2zrngmmgm  45504  srhmsubc  45634  srhmsubcALTV  45652  zlmodzxzsubm  45695  zlmodzxzsub  45696