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  5095  fundif  6541  funcnvqp  6556  fliftfun  7258  wfr3g  8261  omordi  8493  nadd4  8626  naddel12  8628  f1imaen2g  8952  isinf  9165  frfi  9185  frr3g  9668  acndom2  9964  infxp  10124  cff1  10168  isf32lem7  10269  fpwwe2lem11  10552  inawinalem  10600  inar1  10686  grur1  10731  genpnnp  10916  ltexprlem7  10953  prlem936  10958  reclem3pr  10960  1re  11132  addsub4  11424  muladd  11569  lt2add  11622  mullt0  11656  mulnzcnf  11783  divmuldiv  11841  divmul24  11845  divmuleq  11846  recdiv  11847  divadddiv  11856  conjmul  11858  prodgt0  11988  ltmul12a  11997  lemul12b  11998  lediv12a  12035  lediv2a  12036  qmulcl  12880  irrmul  12887  xrrege0  13089  xmulge0  13199  ge0addcl  13376  ge0mulcl  13377  ge0xaddcl  13378  ge0xmulcl  13379  fzass4  13478  fzrev  13503  fzocatel  13645  serge0  13979  expclzlem  14006  expge0  14021  expge1  14022  lt2sq  14056  le2sq  14057  bernneq  14152  ccatw2s1p2  14561  swrdccatin2  14652  cshwleneq  14740  s2eq2seq  14860  wwlktovf1  14880  sqrmo  15174  limsupval2  15403  o1lo12  15461  climrlim2  15470  2clim  15495  climsup  15593  tanaddlem  16091  opeo  16292  omeo  16293  divalglem8  16327  coprmproddvdslem  16589  pcpremul  16771  pcmul  16779  setscom  17107  fpwipodrs  18463  gsumsgrpccat  18765  dfgrp3lem  18968  grplactcnv  18973  resgrpisgrp  19077  ghmpreima  19167  ghmeql  19168  conjghm  19178  pgpfi  19534  rngpropd  20109  srhmsubc  20613  lmodprop2d  20875  cndrng  21353  absabv  21379  xrs1mnd  21395  frlmipval  21734  lmimco  21799  mavmulass  22493  mdetdiaglem  22542  cramerimplem2  22628  opnneissb  23058  cncnpi  23222  pnrmopn  23287  cmpsub  23344  connsub  23365  t1connperf  23380  neitx  23551  txcnmpt  23568  txrest  23575  txdis1cn  23579  tx1stc  23594  qtopcn  23658  trfg  23835  rnelfmlem  23896  flffbas  23939  nmo0  24679  nmoid  24686  cfilfcls  25230  iscmet3lem2  25248  caubl  25264  relcmpcmet  25274  ovolun  25456  ovolicc2lem3  25476  volsup  25513  ioombl1lem4  25518  ismbf3d  25611  mbfimaopnlem  25612  i1faddlem  25650  itgle  25767  ellimc2  25834  ftc1a  26000  dgrmul  26232  itgulm  26373  abelthlem8  26405  ptolemy  26461  logdivlt  26586  cxplt3  26665  cxple3  26666  o1cxp  26941  basellem4  27050  sqf11  27105  lgslem3  27266  lgsdir2  27297  lgsne0  27302  lgsquad3  27354  chpo1ubb  27448  vmadivsumb  27450  rpvmasumlem  27454  dchrisum0re  27480  dchrisum0  27487  selberg2b  27519  selberg3lem2  27525  pntrsumbnd  27533  pntrlog2bnd  27551  nocvxmin  27751  mulsgt0  28140  nnaddscl  28342  nnmulscl  28343  ishpg  28831  axcontlem2  29038  umgr2edg  29282  umgrvad2edg  29286  uhgrspan1  29376  wlkeq  29707  clwwlkccatlem  30064  wwlksext2clwwlk  30132  conngrv2edg  30270  frgrnbnb  30368  frgrwopreglem5lem  30395  frgrwopreglem5ALT  30397  grporcan  30593  blocni  30880  ubthlem3  30947  htthlem  30992  hvsub4  31112  shscli  31392  elspansn4  31648  5oalem2  31730  hosub4  31888  hmops  32095  hmopco  32098  adjadd  32168  hstpyth  32304  hstles  32306  mdsl0  32385  mdslmd1lem2  32401  chirredlem1  32465  chirredlem2  32466  chirredlem3  32467  chirredlem4  32468  mdsymlem6  32483  cdj3lem2b  32512  1stpreimas  32785  irngnzply1  33848  mdetpmtr2  33981  esumpcvgval  34235  signstfvc  34731  noinfepfnregs  35288  satffunlem  35595  mpomulnzcnf  36493  tailfb  36571  isbasisrelowllem1  37560  isbasisrelowllem2  37561  poimirlem14  37835  heicant  37856  mblfinlem4  37861  ismblfin  37862  itg2addnc  37875  ftc1cnnc  37893  filbcmb  37941  prdsbnd  37994  ismtyval  38001  heiborlem8  38019  ghomco  38092  mzpindd  42988  tfsconcatun  43579  oaun3lem1  43616  oaun3lem2  43617  mulltgt0  45267  stoweidlem46  46290  fourierdlem73  46423  cfsetsnfsetf1  47305  iccelpart  47679  bgoldbtbnd  48055  grimco  48135  isubgrgrim  48175  usgrgrtrirex  48196  grlictr  48261  2zrngmmgm  48498  srhmsubcALTV  48571  zlmodzxzsubm  48605  zlmodzxzsub  48606