Theorem ad2ant2r 760

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  disjxiun  5108  fundif  6589  funcnvqp  6604  xpsntpg  7143  fliftfun  7319  wfr3g  8322  omordi  8557  nadd4  8691  naddel12  8693  f1imaen2g  9018  isinf  9232  frfi  9252  frr3g  9735  acndom2  10054  infxp  10213  cff1  10257  isf32lem7  10358  fpwwe2lem11  10641  inawinalem  10689  inar1  10775  grur1  10820  genpnnp  11005  ltexprlem7  11042  prlem936  11047  reclem3pr  11049  1re  11223  addsub4  11516  muladd  11661  lt2add  11714  mullt0  11748  mulnzcnf  11875  divmuldiv  11930  divmul24  11934  divmuleq  11935  recdiv  11936  divadddiv  11945  conjmul  11947  prodgt0  12077  ltmul12a  12086  lemul12b  12087  lediv12a  12123  lediv2a  12124  qmulcl  13007  irrmul  13014  xrrege0  13216  xmulge0  13326  ge0addcl  13503  ge0mulcl  13504  ge0xaddcl  13505  ge0xmulcl  13506  fzass4  13607  fzrev  13632  fzocatel  13775  serge0  14110  expclzlem  14137  expge0  14152  expge1  14153  lt2sq  14187  le2sq  14188  bernneq  14283  ccatw2s1p2  14695  swrdccatin2  14788  cshwleneq  14878  s2eq2seq  14998  wwlktovf1  15018  sqrmo  15326  limsupval2  15555  o1lo12  15613  climrlim2  15622  2clim  15647  climsup  15745  tanaddlem  16244  opeo  16445  omeo  16446  divalglem8  16480  coprmproddvdslem  16742  pcpremul  16925  pcmul  16933  setscom  17262  fpwipodrs  18618  gsumsgrpccat  18936  dfgrp3lem  19148  grplactcnv  19153  resgrpisgrp  19258  ghmpreima  19352  ghmeql  19353  conjghm  19363  pgpfi  19719  rngpropd  20296  srhmsubc  20829  lmodprop2d  21095  cndrng  21601  absabv  21624  xrs1mnd  21640  frlmipval  21979  lmimco  22044  mavmulass  22756  mdetdiaglem  22805  cramerimplem2  22891  opnneissb  23321  cncnpi  23485  pnrmopn  23550  cmpsub  23607  connsub  23628  t1connperf  23643  neitx  23815  txcnmpt  23832  txrest  23839  txdis1cn  23843  tx1stc  23858  qtopcn  23922  trfg  24099  rnelfmlem  24160  flffbas  24203  nmo0  24943  nmoid  24950  cfilfcls  25484  iscmet3lem2  25502  caubl  25518  relcmpcmet  25528  ovolun  25709  ovolicc2lem3  25729  volsup  25766  ioombl1lem4  25771  ismbf3d  25864  mbfimaopnlem  25865  i1faddlem  25903  itgle  26020  ellimc2  26087  ftc1a  26247  dgrmul  26478  itgulm  26622  abelthlem8  26653  ptolemy  26712  logdivlt  26837  cxplt3  26916  cxple3  26917  o1cxp  27190  basellem4  27299  sqf11  27354  lgslem3  27514  lgsdir2  27545  lgsne0  27550  lgsquad3  27602  chpo1ubb  27696  vmadivsumb  27698  rpvmasumlem  27702  dchrisum0re  27728  dchrisum0  27735  selberg2b  27767  selberg3lem2  27773  pntrsumbnd  27781  pntrlog2bnd  27799  nocvxmin  27999  mulsgt0  28388  nnaddscl  28590  nnmulscl  28591  ishpg  29092  axcontlem2  29370  umgr2edg  29617  umgrvad2edg  29621  uhgrspan1  29711  wlkeq  30041  clwwlkccatlem  30407  wwlksext2clwwlk  30475  conngrv2edg  30617  frgrnbnb  30715  frgrwopreglem5lem  30742  frgrwopreglem5ALT  30744  grporcan  30941  blocni  31228  ubthlem3  31295  htthlem  31340  hvsub4  31460  shscli  31740  elspansn4  31996  5oalem2  32078  hosub4  32236  hmops  32443  hmopco  32446  adjadd  32516  hstpyth  32652  hstles  32654  mdsl0  32733  mdslmd1lem2  32749  chirredlem1  32813  chirredlem2  32814  chirredlem3  32815  chirredlem4  32816  mdsymlem6  32831  cdj3lem2b  32860  1stpreimas  33122  irngnzply1  34145  mdetpmtr2  34278  esumpcvgval  34532  signstfvc  35026  noinfepfnregs  35602  satffunlem  35930  nmulprop  36719  nmulel1  36744  mpomulnzcnf  36868  tailfb  36945  isbasisrelowllem1  38058  isbasisrelowllem2  38059  poimirlem14  38342  heicant  38363  mblfinlem4  38368  ismblfin  38369  itg2addnc  38382  ftc1cnnc  38400  filbcmb  38449  prdsbnd  38502  ismtyval  38509  heiborlem8  38527  ghomco  38600  mzpindd  43535  tfsconcatun  44122  oaun3lem1  44159  oaun3lem2  44160  mulltgt0  45800  stoweidlem46  46818  fourierdlem73  46951  cfsetsnfsetf1  47854  iccelpart  48240  bgoldbtbnd  48632  grimco  48712  isubgrgrim  48752  usgrgrtrirex  48773  grlictr  48838  2zrngmmgm  49074  srhmsubcALTV  49147  zlmodzxzsubm  49196  zlmodzxzsub  49197