Theorem ad2ant2r 757

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 727	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantlr 725	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 209  df-an 400

This theorem is referenced by:  disjxiun  5097  fundif  6570  funcnvqp  6585  fliftfun  7296  wfr3g  8300  omordi  8535  nadd4  8669  naddel12  8671  f1imaen2g  8996  isinf  9209  frfi  9229  frr3g  9714  acndom2  10010  infxp  10170  cff1  10215  isf32lem7  10316  fpwwe2lem11  10599  inawinalem  10647  inar1  10733  grur1  10778  genpnnp  10963  ltexprlem7  11000  prlem936  11005  reclem3pr  11007  1re  11181  addsub4  11474  muladd  11619  lt2add  11672  mullt0  11706  mulnzcnf  11833  divmuldiv  11891  divmul24  11895  divmuleq  11896  recdiv  11897  divadddiv  11906  conjmul  11908  prodgt0  12038  ltmul12a  12047  lemul12b  12048  lediv12a  12085  lediv2a  12086  qmulcl  12968  irrmul  12975  xrrege0  13177  xmulge0  13287  ge0addcl  13464  ge0mulcl  13465  ge0xaddcl  13466  ge0xmulcl  13467  fzass4  13567  fzrev  13592  fzocatel  13735  serge0  14069  expclzlem  14096  expge0  14111  expge1  14112  lt2sq  14146  le2sq  14147  bernneq  14242  ccatw2s1p2  14651  swrdccatin2  14742  cshwleneq  14830  s2eq2seq  14950  wwlktovf1  14970  sqrmo  15278  limsupval2  15507  o1lo12  15565  climrlim2  15574  2clim  15599  climsup  15697  tanaddlem  16198  opeo  16399  omeo  16400  divalglem8  16434  coprmproddvdslem  16696  pcpremul  16879  pcmul  16887  setscom  17216  fpwipodrs  18572  gsumsgrpccat  18874  dfgrp3lem  19080  grplactcnv  19085  resgrpisgrp  19189  ghmpreima  19278  ghmeql  19279  conjghm  19289  pgpfi  19645  rngpropd  20220  srhmsubc  20730  lmodprop2d  20991  cndrng  21453  absabv  21476  xrs1mnd  21492  frlmipval  21831  lmimco  21896  mavmulass  22609  mdetdiaglem  22658  cramerimplem2  22744  opnneissb  23174  cncnpi  23338  pnrmopn  23403  cmpsub  23460  connsub  23481  t1connperf  23496  neitx  23667  txcnmpt  23684  txrest  23691  txdis1cn  23695  tx1stc  23710  qtopcn  23774  trfg  23951  rnelfmlem  24012  flffbas  24055  nmo0  24795  nmoid  24802  cfilfcls  25336  iscmet3lem2  25354  caubl  25370  relcmpcmet  25380  ovolun  25561  ovolicc2lem3  25581  volsup  25618  ioombl1lem4  25623  ismbf3d  25716  mbfimaopnlem  25717  i1faddlem  25755  itgle  25872  ellimc2  25939  ftc1a  26099  dgrmul  26330  itgulm  26471  abelthlem8  26502  ptolemy  26561  logdivlt  26686  cxplt3  26765  cxple3  26766  o1cxp  27039  basellem4  27148  sqf11  27203  lgslem3  27363  lgsdir2  27394  lgsne0  27399  lgsquad3  27451  chpo1ubb  27545  vmadivsumb  27547  rpvmasumlem  27551  dchrisum0re  27577  dchrisum0  27584  selberg2b  27616  selberg3lem2  27622  pntrsumbnd  27630  pntrlog2bnd  27648  nocvxmin  27848  mulsgt0  28237  nnaddscl  28439  nnmulscl  28440  ishpg  28932  axcontlem2  29166  umgr2edg  29410  umgrvad2edg  29414  uhgrspan1  29504  wlkeq  29834  clwwlkccatlem  30191  wwlksext2clwwlk  30259  conngrv2edg  30397  frgrnbnb  30495  frgrwopreglem5lem  30522  frgrwopreglem5ALT  30524  grporcan  30721  blocni  31008  ubthlem3  31075  htthlem  31120  hvsub4  31240  shscli  31520  elspansn4  31776  5oalem2  31858  hosub4  32016  hmops  32223  hmopco  32226  adjadd  32296  hstpyth  32432  hstles  32434  mdsl0  32513  mdslmd1lem2  32529  chirredlem1  32593  chirredlem2  32594  chirredlem3  32595  chirredlem4  32596  mdsymlem6  32611  cdj3lem2b  32640  1stpreimas  32908  irngnzply1  33988  mdetpmtr2  34121  esumpcvgval  34375  signstfvc  34868  noinfepfnregs  35428  satffunlem  35751  nmulprop  36540  mpomulnzcnf  36659  tailfb  36737  isbasisrelowllem1  37849  isbasisrelowllem2  37850  poimirlem14  38133  heicant  38154  mblfinlem4  38159  ismblfin  38160  itg2addnc  38173  ftc1cnnc  38191  filbcmb  38239  prdsbnd  38292  ismtyval  38299  heiborlem8  38317  ghomco  38390  mzpindd  43327  tfsconcatun  43914  oaun3lem1  43951  oaun3lem2  43952  mulltgt0  45602  stoweidlem46  46620  fourierdlem73  46753  cfsetsnfsetf1  47653  iccelpart  48039  bgoldbtbnd  48431  grimco  48511  isubgrgrim  48551  usgrgrtrirex  48572  grlictr  48637  2zrngmmgm  48874  srhmsubcALTV  48947  zlmodzxzsubm  48981  zlmodzxzsub  48982