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  5107  fundif  6568  funcnvqp  6583  fliftfun  7290  wfr3g  8301  omordi  8533  nadd4  8665  naddel12  8667  f1imaen2g  8989  isinf  9214  isinfOLD  9215  frfi  9239  frr3g  9716  acndom2  10014  infxp  10174  cff1  10218  isf32lem7  10319  fpwwe2lem11  10601  inawinalem  10649  inar1  10735  grur1  10780  genpnnp  10965  ltexprlem7  11002  prlem936  11007  reclem3pr  11009  1re  11181  addsub4  11472  muladd  11617  lt2add  11670  mullt0  11704  mulnzcnf  11831  divmuldiv  11889  divmul24  11893  divmuleq  11894  recdiv  11895  divadddiv  11904  conjmul  11906  prodgt0  12036  ltmul12a  12045  lemul12b  12046  lediv12a  12083  lediv2a  12084  qmulcl  12933  irrmul  12940  xrrege0  13141  xmulge0  13251  ge0addcl  13428  ge0mulcl  13429  ge0xaddcl  13430  ge0xmulcl  13431  fzass4  13530  fzrev  13555  fzocatel  13697  serge0  14028  expclzlem  14055  expge0  14070  expge1  14071  lt2sq  14105  le2sq  14106  bernneq  14201  ccatw2s1p2  14609  swrdccatin2  14701  cshwleneq  14789  s2eq2seq  14910  wwlktovf1  14930  sqrmo  15224  limsupval2  15453  o1lo12  15511  climrlim2  15520  2clim  15545  climsup  15643  tanaddlem  16141  opeo  16342  omeo  16343  divalglem8  16377  coprmproddvdslem  16639  pcpremul  16821  pcmul  16829  setscom  17157  fpwipodrs  18506  gsumsgrpccat  18774  dfgrp3lem  18977  grplactcnv  18982  resgrpisgrp  19086  ghmpreima  19177  ghmeql  19178  conjghm  19188  pgpfi  19542  rngpropd  20090  srhmsubc  20596  lmodprop2d  20837  cndrng  21317  xrs1mnd  21328  absabv  21348  frlmipval  21695  lmimco  21760  mavmulass  22443  mdetdiaglem  22492  cramerimplem2  22578  opnneissb  23008  cncnpi  23172  pnrmopn  23237  cmpsub  23294  connsub  23315  t1connperf  23330  neitx  23501  txcnmpt  23518  txrest  23525  txdis1cn  23529  tx1stc  23544  qtopcn  23608  trfg  23785  rnelfmlem  23846  flffbas  23889  nmo0  24630  nmoid  24637  cfilfcls  25181  iscmet3lem2  25199  caubl  25215  relcmpcmet  25225  ovolun  25407  ovolicc2lem3  25427  volsup  25464  ioombl1lem4  25469  ismbf3d  25562  mbfimaopnlem  25563  i1faddlem  25601  itgle  25718  ellimc2  25785  ftc1a  25951  dgrmul  26183  itgulm  26324  abelthlem8  26356  ptolemy  26412  logdivlt  26537  cxplt3  26616  cxple3  26617  o1cxp  26892  basellem4  27001  sqf11  27056  lgslem3  27217  lgsdir2  27248  lgsne0  27253  lgsquad3  27305  chpo1ubb  27399  vmadivsumb  27401  rpvmasumlem  27405  dchrisum0re  27431  dchrisum0  27438  selberg2b  27470  selberg3lem2  27476  pntrsumbnd  27484  pntrlog2bnd  27502  nocvxmin  27697  mulsgt0  28054  nnaddscl  28245  nnmulscl  28246  ishpg  28693  axcontlem2  28899  umgr2edg  29143  umgrvad2edg  29147  uhgrspan1  29237  wlkeq  29569  clwwlkccatlem  29925  wwlksext2clwwlk  29993  conngrv2edg  30131  frgrnbnb  30229  frgrwopreglem5lem  30256  frgrwopreglem5ALT  30258  grporcan  30454  blocni  30741  ubthlem3  30808  htthlem  30853  hvsub4  30973  shscli  31253  elspansn4  31509  5oalem2  31591  hosub4  31749  hmops  31956  hmopco  31959  adjadd  32029  hstpyth  32165  hstles  32167  mdsl0  32246  mdslmd1lem2  32262  chirredlem1  32326  chirredlem2  32327  chirredlem3  32328  chirredlem4  32329  mdsymlem6  32344  cdj3lem2b  32373  1stpreimas  32636  irngnzply1  33693  mdetpmtr2  33821  esumpcvgval  34075  signstfvc  34572  satffunlem  35395  mpomulnzcnf  36294  tailfb  36372  isbasisrelowllem1  37350  isbasisrelowllem2  37351  poimirlem14  37635  heicant  37656  mblfinlem4  37661  ismblfin  37662  itg2addnc  37675  ftc1cnnc  37693  filbcmb  37741  prdsbnd  37794  ismtyval  37801  heiborlem8  37819  ghomco  37892  mzpindd  42741  tfsconcatun  43333  oaun3lem1  43370  oaun3lem2  43371  mulltgt0  45023  stoweidlem46  46051  fourierdlem73  46184  cfsetsnfsetf1  47064  iccelpart  47438  bgoldbtbnd  47814  grimco  47893  isubgrgrim  47933  usgrgrtrirex  47953  grlictr  48011  2zrngmmgm  48244  srhmsubcALTV  48317  zlmodzxzsubm  48351  zlmodzxzsub  48352