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  5099  fundif  6594  funcnvqp  6609  xpsntpg  7149  fliftfun  7324  wfr3g  8345  omordi  8582  nadd4  8716  naddel12  8718  f1imaen2g  9050  isinf  9264  frfi  9284  frr3g  9767  acndom2  10140  infxp  10299  cff1  10343  isf32lem7  10444  fpwwe2lem11  10733  inawinalem  10781  inar1  10867  grur1  10912  genpnnp  11097  ltexprlem7  11134  prlem936  11139  reclem3pr  11141  1re  11315  addsub4  11608  muladd  11755  lt2add  11808  mullt0  11842  mulnzcnf  11969  divmuldiv  12024  divmul24  12028  divmuleq  12029  recdiv  12030  divadddiv  12039  conjmul  12041  prodgt0  12171  ltmul12a  12180  lemul12b  12181  lediv12a  12217  lediv2a  12218  qmulcl  13102  irrmul  13109  xrrege0  13311  xmulge0  13421  ge0addcl  13598  ge0mulcl  13599  ge0xaddcl  13600  ge0xmulcl  13601  fzass4  13703  fzrev  13728  fzocatel  13871  serge0  14206  expclzlem  14233  expge0  14248  expge1  14249  lt2sq  14283  le2sq  14284  bernneq  14380  ccatw2s1p2  14793  swrdccatin2  14886  cshwleneq  14976  s2eq2seq  15097  wwlktovf1  15119  sqrmo  15427  limsupval2  15656  o1lo12  15714  climrlim2  15723  2clim  15748  climsup  15846  tanaddlem  16343  opeo  16544  omeo  16545  divalglem8  16579  coprmproddvdslem  16846  pcpremul  17030  pcmul  17038  setscom  17367  fpwipodrs  18723  gsumsgrpccat  19045  dfgrp3lem  19257  grplactcnv  19262  resgrpisgrp  19367  ghmpreima  19461  ghmeql  19462  conjghm  19472  pgpfi  19828  rngpropd  20405  srhmsubc  20941  lmodprop2d  21208  cndrng  21716  absabv  21739  xrs1mnd  21755  frlmipval  22094  lmimco  22159  mavmulass  22873  mdetdiaglem  22922  cramerimplem2  23011  opnneissb  23441  cncnpi  23605  pnrmopn  23670  cmpsub  23727  connsub  23748  t1connperf  23763  neitx  23935  txcnmpt  23952  txrest  23959  txdis1cn  23963  tx1stc  23978  qtopcn  24042  trfg  24219  rnelfmlem  24280  flffbas  24323  nmo0  25063  nmoid  25070  cfilfcls  25604  iscmet3lem2  25622  caubl  25638  relcmpcmet  25648  ovolun  25829  ovolicc2lem3  25849  volsup  25886  ioombl1lem4  25891  ismbf3d  25984  mbfimaopnlem  25985  i1faddlem  26023  itgle  26139  ellimc2  26206  ftc1a  26366  dgrmul  26598  itgulm  26744  abelthlem8  26775  ptolemy  26834  logdivlt  26958  cxplt3  27037  cxple3  27038  o1cxp  27311  basellem4  27420  sqf11  27475  lgslem3  27635  lgsdir2  27666  lgsne0  27671  lgsquad3  27723  chpo1ubb  27817  vmadivsumb  27819  rpvmasumlem  27823  dchrisum0re  27849  dchrisum0  27856  selberg2b  27888  selberg3lem2  27894  pntrsumbnd  27902  pntrlog2bnd  27920  nocvxmin  28150  mulsgt0  28539  nnaddscl  28741  nnmulscl  28742  ishpg  29246  axcontlem2  29552  umgr2edg  29799  umgrvad2edg  29803  uhgrspan1  29893  wlkeq  30223  clwwlkccatlem  30589  wwlksext2clwwlk  30657  conngrv2edg  30805  frgrnbnb  30903  frgrwopreglem5lem  30930  frgrwopreglem5ALT  30932  grporcan  31129  blocni  31416  ubthlem3  31483  htthlem  31528  hvsub4  31648  shscli  31928  elspansn4  32184  5oalem2  32266  hosub4  32424  hmops  32631  hmopco  32634  adjadd  32704  hstpyth  32840  hstles  32842  mdsl0  32921  mdslmd1lem2  32937  chirredlem1  33001  chirredlem2  33002  chirredlem3  33003  chirredlem4  33004  mdsymlem6  33019  cdj3lem2b  33048  1stpreimas  33350  irngnzply1  34373  mdetpmtr2  34506  esumpcvgval  34760  signstfvc  35253  noinfepfnregs  35868  satffunlem  36284  nmulprop  37063  nmulel1  37088  mpomulnzcnf  37212  tailfb  37289  isbasisrelowllem1  38415  isbasisrelowllem2  38416  poimirlem14  38689  heicant  38710  mblfinlem4  38715  ismblfin  38716  itg2addnc  38729  ftc1cnnc  38747  filbcmb  38811  prdsbnd  38864  ismtyval  38871  heiborlem8  38889  ghomco  38962  mzpindd  43894  tfsconcatun  44476  oaun3lem1  44513  oaun3lem2  44514  mulltgt0  46175  stoweidlem46  47192  fourierdlem73  47325  cfsetsnfsetf1  48265  iccelpart  48651  bgoldbtbnd  49043  grimco  49123  isubgrgrim  49163  usgrgrtrirex  49184  grlictr  49249  2zrngmmgm  49485  srhmsubcALTV  49558  zlmodzxzsubm  49607  zlmodzxzsub  49608