Theorem ad2ant2r 746

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  disjxiun  5027  fundif  6373  funcnvqp  6388  foco  6577  fliftfun  7044  wfr3g  7936  omordi  8175  f1imaen2g  8553  isinf  8715  frfi  8747  acndom2  9465  infxp  9626  cff1  9669  isf32lem7  9770  fpwwe2lem12  10052  inawinalem  10100  inar1  10186  grur1  10231  genpnnp  10416  ltexprlem7  10453  prlem936  10458  reclem3pr  10460  1re  10630  addsub4  10918  muladd  11061  lt2add  11114  mullt0  11148  mulnzcnopr  11275  divmuldiv  11329  divmul24  11333  divmuleq  11334  recdiv  11335  divadddiv  11344  conjmul  11346  prodgt0  11476  ltmul12a  11485  lemul12b  11486  lediv12a  11522  lediv2a  11523  qmulcl  12354  irrmul  12361  xrrege0  12555  xmulge0  12665  ge0addcl  12838  ge0mulcl  12839  ge0xaddcl  12840  ge0xmulcl  12841  fzass4  12940  fzrev  12965  fzocatel  13096  serge0  13420  expclzlem  13449  expge0  13461  expge1  13462  lt2sq  13494  le2sq  13495  bernneq  13586  ccatw2s1p1OLD  13987  ccatw2s1p2  13988  swrdccatin2  14082  cshwleneq  14170  s2eq2seq  14290  wwlktovf1  14312  sqrmo  14603  limsupval2  14829  o1lo12  14887  climrlim2  14896  2clim  14921  climsup  15018  tanaddlem  15511  opeo  15706  omeo  15707  divalglem8  15741  coprmproddvdslem  15996  pcpremul  16170  pcmul  16178  setscom  16519  fpwipodrs  17766  gsumsgrpccat  17996  dfgrp3lem  18189  grplactcnv  18194  resgrpisgrp  18292  ghmpreima  18372  ghmeql  18373  conjghm  18381  pgpfi  18722  lmodprop2d  19689  lidlmcl  19983  xrs1mnd  20129  absabv  20148  frlmipval  20468  lmimco  20533  mavmulass  21154  mdetdiaglem  21203  cramerimplem2  21289  opnneissb  21719  cncnpi  21883  pnrmopn  21948  cmpsub  22005  connsub  22026  t1connperf  22041  neitx  22212  txcnmpt  22229  txrest  22236  txdis1cn  22240  tx1stc  22255  qtopcn  22319  trfg  22496  rnelfmlem  22557  flffbas  22600  nmo0  23341  nmoid  23348  cfilfcls  23878  iscmet3lem2  23896  caubl  23912  relcmpcmet  23922  ovolun  24103  ovolicc2lem3  24123  volsup  24160  ioombl1lem4  24165  ismbf3d  24258  mbfimaopnlem  24259  i1faddlem  24297  itgle  24413  ellimc2  24480  ftc1a  24640  dgrmul  24867  itgulm  25003  abelthlem8  25034  ptolemy  25089  logdivlt  25212  cxplt3  25291  cxple3  25292  o1cxp  25560  basellem4  25669  sqf11  25724  lgslem3  25883  lgsdir2  25914  lgsne0  25919  lgsquad3  25971  chpo1ubb  26065  vmadivsumb  26067  rpvmasumlem  26071  dchrisum0re  26097  dchrisum0  26104  selberg2b  26136  selberg3lem2  26142  pntrsumbnd  26150  pntrlog2bnd  26168  ishpg  26553  axcontlem2  26759  umgr2edg  26999  umgrvad2edg  27003  uhgrspan1  27093  wlkeq  27423  clwwlkccatlem  27774  wwlksext2clwwlk  27842  conngrv2edg  27980  frgrnbnb  28078  frgrwopreglem5lem  28105  frgrwopreglem5ALT  28107  grporcan  28301  blocni  28588  ubthlem3  28655  htthlem  28700  hvsub4  28820  shscli  29100  elspansn4  29356  5oalem2  29438  hosub4  29596  hmops  29803  hmopco  29806  adjadd  29876  hstpyth  30012  hstles  30014  mdsl0  30093  mdslmd1lem2  30109  chirredlem1  30173  chirredlem2  30174  chirredlem3  30175  chirredlem4  30176  mdsymlem6  30191  cdj3lem2b  30220  1stpreimas  30465  mdetpmtr2  31177  esumpcvgval  31447  signstfvc  31954  satffunlem  32761  frr3g  33234  nocvxmin  33361  tailfb  33838  isbasisrelowllem1  34772  isbasisrelowllem2  34773  poimirlem14  35071  heicant  35092  mblfinlem4  35097  ismblfin  35098  itg2addnc  35111  ftc1cnnc  35129  filbcmb  35178  prdsbnd  35231  ismtyval  35238  heiborlem8  35256  ghomco  35329  mzpindd  39687  mulltgt0  41651  stoweidlem46  42688  fourierdlem73  42821  iccelpart  43950  bgoldbtbnd  44327  2zrngmmgm  44570  srhmsubc  44700  srhmsubcALTV  44718  zlmodzxzsubm  44761  zlmodzxzsub  44762