Theorem ad2ant2r 753

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

Syntax hints:   → wi 4   ∧ wa 384

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

This theorem is referenced by:  nanassOLD  1632  disjxiun  4808  fundif  6118  funcnvqp  6133  foco  6312  fliftfun  6758  wfr3g  7620  omordi  7855  f1imaen2g  8225  isinf  8384  frfi  8416  acndom2  9132  infxp  9294  cff1  9337  isf32lem7  9438  fpwwe2lem12  9720  inawinalem  9768  inar1  9854  grur1  9899  genpnnp  10084  ltexprlem7  10121  prlem936  10126  reclem3pr  10128  1re  10297  addsub4  10583  muladd  10721  lt2add  10772  mullt0  10806  mulnzcnopr  10932  divmuldiv  10984  divmul24  10988  divmuleq  10989  recdiv  10990  divadddiv  10999  conjmul  11001  prodgt0  11127  ltmul12a  11138  lemul12b  11139  lediv12a  11175  lediv2a  11176  qmulcl  12014  irrmul  12021  xrrege0  12214  xmulge0  12323  ge0addcl  12495  ge0mulcl  12496  ge0xaddcl  12497  ge0xmulcl  12498  fzass4  12593  fzrev  12617  fzocatel  12747  serge0  13069  expclzlem  13098  expge0  13110  expge1  13111  lt2sq  13151  le2sq  13152  bernneq  13204  ccatw2s1p1  13620  ccatw2s1p2  13621  cshwleneq  13862  s2eq2seq  13982  sqrmo  14293  limsupval2  14512  o1lo12  14570  climrlim2  14579  2clim  14604  climsup  14701  tanaddlem  15194  opeo  15387  omeo  15388  divalglem8  15421  coprmproddvdslem  15672  pcpremul  15843  pcmul  15851  setscom  16191  fpwipodrs  17446  dfgrp3lem  17796  grplactcnv  17801  resgrpisgrp  17895  ghmpreima  17962  ghmeql  17963  conjghm  17971  pgpfi  18300  lmodprop2d  19210  lidlmcl  19507  xrs1mnd  20073  absabv  20092  frlmipval  20410  lmimco  20475  mavmulass  20648  mdetdiaglem  20697  cramerimplem2  20785  opnneissb  21214  cncnpi  21378  pnrmopn  21443  cmpsub  21499  connsub  21520  t1connperf  21535  neitx  21706  txcnmpt  21723  txrest  21730  txdis1cn  21734  tx1stc  21749  qtopcn  21813  trfg  21990  rnelfmlem  22051  flffbas  22094  nmo0  22834  nmoid  22841  cfilfcls  23367  iscmet3lem2  23385  caubl  23401  relcmpcmet  23411  ovolun  23573  ovolicc2lem3  23593  volsup  23630  ioombl1lem4  23635  ismbf3d  23728  mbfimaopnlem  23729  i1faddlem  23767  itgle  23883  ellimc2  23948  ftc1a  24107  dgrmul  24333  itgulm  24469  abelthlem8  24500  ptolemy  24556  logdivlt  24674  cxplt3  24753  cxple3  24754  o1cxp  25008  basellem4  25117  sqf11  25172  lgslem3  25331  lgsdir2  25362  lgsne0  25367  lgsquad3  25419  chpo1ubb  25477  vmadivsumb  25479  rpvmasumlem  25483  dchrisum0re  25509  dchrisum0  25516  selberg2b  25548  selberg3lem2  25554  pntrsumbnd  25562  pntrlog2bnd  25580  axcontlem2  26152  umgr2edg  26395  umgrvad2edg  26399  uhgrspan1  26490  wlkeq  26836  wwlksext2clwwlk  27327  wwlksext2clwwlkOLD  27328  conngrv2edg  27493  frgrnbnb  27596  frgrwopreglem5lem  27623  frgrwopreglem5ALT  27625  grporcan  27852  blocni  28139  ubthlem3  28207  htthlem  28253  hvsub4  28373  shscli  28655  elspansn4  28911  5oalem2  28993  hosub4  29151  hmops  29358  hmopco  29361  adjadd  29431  hstpyth  29567  hstles  29569  mdsl0  29648  mdslmd1lem2  29664  chirredlem1  29728  chirredlem2  29729  chirredlem3  29730  chirredlem4  29731  mdsymlem6  29746  cdj3lem2b  29775  1stpreimas  29955  mdetpmtr2  30360  esumpcvgval  30610  frr3g  32246  nocvxmin  32361  tailfb  32838  isbasisrelowllem1  33659  isbasisrelowllem2  33660  poimirlem14  33870  heicant  33891  mblfinlem4  33896  ismblfin  33897  itg2addnc  33910  ftc1cnnc  33930  filbcmb  33981  prdsbnd  34037  ismtyval  34044  heiborlem8  34062  ghomco  34135  mzpindd  38013  mulltgt0  39859  stoweidlem46  40926  fourierdlem73  41059  iccelpart  42129  bgoldbtbnd  42399  2zrngmmgm  42641  srhmsubc  42771  srhmsubcALTV  42789  zlmodzxzsubm  42832  zlmodzxzsub  42833