Theorem ad2ant2r 747

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  disjxiun  5099  fundif  6549  funcnvqp  6564  fliftfun  7269  wfr3g  8275  omordi  8507  nadd4  8639  naddel12  8641  f1imaen2g  8963  isinf  9183  isinfOLD  9184  frfi  9208  frr3g  9685  acndom2  9983  infxp  10143  cff1  10187  isf32lem7  10288  fpwwe2lem11  10570  inawinalem  10618  inar1  10704  grur1  10749  genpnnp  10934  ltexprlem7  10971  prlem936  10976  reclem3pr  10978  1re  11150  addsub4  11441  muladd  11586  lt2add  11639  mullt0  11673  mulnzcnf  11800  divmuldiv  11858  divmul24  11862  divmuleq  11863  recdiv  11864  divadddiv  11873  conjmul  11875  prodgt0  12005  ltmul12a  12014  lemul12b  12015  lediv12a  12052  lediv2a  12053  qmulcl  12902  irrmul  12909  xrrege0  13110  xmulge0  13220  ge0addcl  13397  ge0mulcl  13398  ge0xaddcl  13399  ge0xmulcl  13400  fzass4  13499  fzrev  13524  fzocatel  13666  serge0  13997  expclzlem  14024  expge0  14039  expge1  14040  lt2sq  14074  le2sq  14075  bernneq  14170  ccatw2s1p2  14578  swrdccatin2  14670  cshwleneq  14758  s2eq2seq  14879  wwlktovf1  14899  sqrmo  15193  limsupval2  15422  o1lo12  15480  climrlim2  15489  2clim  15514  climsup  15612  tanaddlem  16110  opeo  16311  omeo  16312  divalglem8  16346  coprmproddvdslem  16608  pcpremul  16790  pcmul  16798  setscom  17126  fpwipodrs  18475  gsumsgrpccat  18743  dfgrp3lem  18946  grplactcnv  18951  resgrpisgrp  19055  ghmpreima  19146  ghmeql  19147  conjghm  19157  pgpfi  19511  rngpropd  20059  srhmsubc  20565  lmodprop2d  20806  cndrng  21286  xrs1mnd  21297  absabv  21317  frlmipval  21664  lmimco  21729  mavmulass  22412  mdetdiaglem  22461  cramerimplem2  22547  opnneissb  22977  cncnpi  23141  pnrmopn  23206  cmpsub  23263  connsub  23284  t1connperf  23299  neitx  23470  txcnmpt  23487  txrest  23494  txdis1cn  23498  tx1stc  23513  qtopcn  23577  trfg  23754  rnelfmlem  23815  flffbas  23858  nmo0  24599  nmoid  24606  cfilfcls  25150  iscmet3lem2  25168  caubl  25184  relcmpcmet  25194  ovolun  25376  ovolicc2lem3  25396  volsup  25433  ioombl1lem4  25438  ismbf3d  25531  mbfimaopnlem  25532  i1faddlem  25570  itgle  25687  ellimc2  25754  ftc1a  25920  dgrmul  26152  itgulm  26293  abelthlem8  26325  ptolemy  26381  logdivlt  26506  cxplt3  26585  cxple3  26586  o1cxp  26861  basellem4  26970  sqf11  27025  lgslem3  27186  lgsdir2  27217  lgsne0  27222  lgsquad3  27274  chpo1ubb  27368  vmadivsumb  27370  rpvmasumlem  27374  dchrisum0re  27400  dchrisum0  27407  selberg2b  27439  selberg3lem2  27445  pntrsumbnd  27453  pntrlog2bnd  27471  nocvxmin  27666  mulsgt0  28023  nnaddscl  28214  nnmulscl  28215  ishpg  28662  axcontlem2  28868  umgr2edg  29112  umgrvad2edg  29116  uhgrspan1  29206  wlkeq  29537  clwwlkccatlem  29891  wwlksext2clwwlk  29959  conngrv2edg  30097  frgrnbnb  30195  frgrwopreglem5lem  30222  frgrwopreglem5ALT  30224  grporcan  30420  blocni  30707  ubthlem3  30774  htthlem  30819  hvsub4  30939  shscli  31219  elspansn4  31475  5oalem2  31557  hosub4  31715  hmops  31922  hmopco  31925  adjadd  31995  hstpyth  32131  hstles  32133  mdsl0  32212  mdslmd1lem2  32228  chirredlem1  32292  chirredlem2  32293  chirredlem3  32294  chirredlem4  32295  mdsymlem6  32310  cdj3lem2b  32339  1stpreimas  32602  irngnzply1  33659  mdetpmtr2  33787  esumpcvgval  34041  signstfvc  34538  satffunlem  35361  mpomulnzcnf  36260  tailfb  36338  isbasisrelowllem1  37316  isbasisrelowllem2  37317  poimirlem14  37601  heicant  37622  mblfinlem4  37627  ismblfin  37628  itg2addnc  37641  ftc1cnnc  37659  filbcmb  37707  prdsbnd  37760  ismtyval  37767  heiborlem8  37785  ghomco  37858  mzpindd  42707  tfsconcatun  43299  oaun3lem1  43336  oaun3lem2  43337  mulltgt0  44989  stoweidlem46  46017  fourierdlem73  46150  cfsetsnfsetf1  47033  iccelpart  47407  bgoldbtbnd  47783  grimco  47862  isubgrgrim  47902  usgrgrtrirex  47922  grlictr  47980  2zrngmmgm  48213  srhmsubcALTV  48286  zlmodzxzsubm  48320  zlmodzxzsub  48321