Theorem ad2ant2r 759

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  disjxiun  5108  fundif  6586  funcnvqp  6601  fliftfun  7311  wfr3g  8316  omordi  8551  nadd4  8685  naddel12  8687  f1imaen2g  9012  isinf  9225  frfi  9245  frr3g  9728  acndom2  10038  infxp  10197  cff1  10242  isf32lem7  10343  fpwwe2lem11  10626  inawinalem  10674  inar1  10760  grur1  10805  genpnnp  10990  ltexprlem7  11027  prlem936  11032  reclem3pr  11034  1re  11208  addsub4  11501  muladd  11646  lt2add  11699  mullt0  11733  mulnzcnf  11860  divmuldiv  11915  divmul24  11919  divmuleq  11920  recdiv  11921  divadddiv  11930  conjmul  11932  prodgt0  12062  ltmul12a  12071  lemul12b  12072  lediv12a  12108  lediv2a  12109  qmulcl  12991  irrmul  12998  xrrege0  13200  xmulge0  13310  ge0addcl  13487  ge0mulcl  13488  ge0xaddcl  13489  ge0xmulcl  13490  fzass4  13590  fzrev  13615  fzocatel  13758  serge0  14092  expclzlem  14119  expge0  14134  expge1  14135  lt2sq  14169  le2sq  14170  bernneq  14265  ccatw2s1p2  14675  swrdccatin2  14766  cshwleneq  14854  s2eq2seq  14974  wwlktovf1  14994  sqrmo  15302  limsupval2  15531  o1lo12  15589  climrlim2  15598  2clim  15623  climsup  15721  tanaddlem  16222  opeo  16423  omeo  16424  divalglem8  16458  coprmproddvdslem  16720  pcpremul  16903  pcmul  16911  setscom  17240  fpwipodrs  18596  gsumsgrpccat  18899  dfgrp3lem  19104  grplactcnv  19109  resgrpisgrp  19214  ghmpreima  19308  ghmeql  19309  conjghm  19319  pgpfi  19675  rngpropd  20252  srhmsubc  20765  lmodprop2d  21023  cndrng  21520  absabv  21543  xrs1mnd  21559  frlmipval  21898  lmimco  21963  mavmulass  22675  mdetdiaglem  22724  cramerimplem2  22810  opnneissb  23240  cncnpi  23404  pnrmopn  23469  cmpsub  23526  connsub  23547  t1connperf  23562  neitx  23733  txcnmpt  23750  txrest  23757  txdis1cn  23761  tx1stc  23776  qtopcn  23840  trfg  24017  rnelfmlem  24078  flffbas  24121  nmo0  24861  nmoid  24868  cfilfcls  25402  iscmet3lem2  25420  caubl  25436  relcmpcmet  25446  ovolun  25627  ovolicc2lem3  25647  volsup  25684  ioombl1lem4  25689  ismbf3d  25782  mbfimaopnlem  25783  i1faddlem  25821  itgle  25938  ellimc2  26005  ftc1a  26165  dgrmul  26396  itgulm  26537  abelthlem8  26568  ptolemy  26627  logdivlt  26752  cxplt3  26831  cxple3  26832  o1cxp  27105  basellem4  27214  sqf11  27269  lgslem3  27429  lgsdir2  27460  lgsne0  27465  lgsquad3  27517  chpo1ubb  27611  vmadivsumb  27613  rpvmasumlem  27617  dchrisum0re  27643  dchrisum0  27650  selberg2b  27682  selberg3lem2  27688  pntrsumbnd  27696  pntrlog2bnd  27714  nocvxmin  27914  mulsgt0  28303  nnaddscl  28505  nnmulscl  28506  ishpg  29000  axcontlem2  29256  umgr2edg  29500  umgrvad2edg  29504  uhgrspan1  29594  wlkeq  29924  clwwlkccatlem  30281  wwlksext2clwwlk  30349  conngrv2edg  30487  frgrnbnb  30585  frgrwopreglem5lem  30612  frgrwopreglem5ALT  30614  grporcan  30811  blocni  31098  ubthlem3  31165  htthlem  31210  hvsub4  31330  shscli  31610  elspansn4  31866  5oalem2  31948  hosub4  32106  hmops  32313  hmopco  32316  adjadd  32386  hstpyth  32522  hstles  32524  mdsl0  32603  mdslmd1lem2  32619  chirredlem1  32683  chirredlem2  32684  chirredlem3  32685  chirredlem4  32686  mdsymlem6  32701  cdj3lem2b  32730  1stpreimas  32992  irngnzply1  34026  mdetpmtr2  34159  esumpcvgval  34413  signstfvc  34906  noinfepfnregs  35478  satffunlem  35826  nmulprop  36615  mpomulnzcnf  36734  tailfb  36811  isbasisrelowllem1  37924  isbasisrelowllem2  37925  poimirlem14  38208  heicant  38229  mblfinlem4  38234  ismblfin  38235  itg2addnc  38248  ftc1cnnc  38266  filbcmb  38314  prdsbnd  38367  ismtyval  38374  heiborlem8  38392  ghomco  38465  mzpindd  43404  tfsconcatun  43991  oaun3lem1  44028  oaun3lem2  44029  mulltgt0  45669  stoweidlem46  46687  fourierdlem73  46820  cfsetsnfsetf1  47720  iccelpart  48106  bgoldbtbnd  48498  grimco  48578  isubgrgrim  48618  usgrgrtrirex  48639  grlictr  48704  2zrngmmgm  48941  srhmsubcALTV  49014  zlmodzxzsubm  49059  zlmodzxzsub  49060