Theorem ad2ant2r 748

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 718	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantlr 716	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  5082  fundif  6547  funcnvqp  6562  fliftfun  7267  wfr3g  8269  omordi  8501  nadd4  8634  naddel12  8636  f1imaen2g  8962  isinf  9175  frfi  9195  frr3g  9680  acndom2  9976  infxp  10136  cff1  10180  isf32lem7  10281  fpwwe2lem11  10564  inawinalem  10612  inar1  10698  grur1  10743  genpnnp  10928  ltexprlem7  10965  prlem936  10970  reclem3pr  10972  1re  11144  addsub4  11437  muladd  11582  lt2add  11635  mullt0  11669  mulnzcnf  11796  divmuldiv  11855  divmul24  11859  divmuleq  11860  recdiv  11861  divadddiv  11870  conjmul  11872  prodgt0  12002  ltmul12a  12011  lemul12b  12012  lediv12a  12049  lediv2a  12050  qmulcl  12917  irrmul  12924  xrrege0  13126  xmulge0  13236  ge0addcl  13413  ge0mulcl  13414  ge0xaddcl  13415  ge0xmulcl  13416  fzass4  13516  fzrev  13541  fzocatel  13684  serge0  14018  expclzlem  14045  expge0  14060  expge1  14061  lt2sq  14095  le2sq  14096  bernneq  14191  ccatw2s1p2  14600  swrdccatin2  14691  cshwleneq  14779  s2eq2seq  14899  wwlktovf1  14919  sqrmo  15213  limsupval2  15442  o1lo12  15500  climrlim2  15509  2clim  15534  climsup  15632  tanaddlem  16133  opeo  16334  omeo  16335  divalglem8  16369  coprmproddvdslem  16631  pcpremul  16814  pcmul  16822  setscom  17150  fpwipodrs  18506  gsumsgrpccat  18808  dfgrp3lem  19014  grplactcnv  19019  resgrpisgrp  19123  ghmpreima  19213  ghmeql  19214  conjghm  19224  pgpfi  19580  rngpropd  20155  srhmsubc  20657  lmodprop2d  20919  cndrng  21381  absabv  21404  xrs1mnd  21420  frlmipval  21759  lmimco  21824  mavmulass  22514  mdetdiaglem  22563  cramerimplem2  22649  opnneissb  23079  cncnpi  23243  pnrmopn  23308  cmpsub  23365  connsub  23386  t1connperf  23401  neitx  23572  txcnmpt  23589  txrest  23596  txdis1cn  23600  tx1stc  23615  qtopcn  23679  trfg  23856  rnelfmlem  23917  flffbas  23960  nmo0  24700  nmoid  24707  cfilfcls  25241  iscmet3lem2  25259  caubl  25275  relcmpcmet  25285  ovolun  25466  ovolicc2lem3  25486  volsup  25523  ioombl1lem4  25528  ismbf3d  25621  mbfimaopnlem  25622  i1faddlem  25660  itgle  25777  ellimc2  25844  ftc1a  26004  dgrmul  26235  itgulm  26373  abelthlem8  26404  ptolemy  26460  logdivlt  26585  cxplt3  26664  cxple3  26665  o1cxp  26938  basellem4  27047  sqf11  27102  lgslem3  27262  lgsdir2  27293  lgsne0  27298  lgsquad3  27350  chpo1ubb  27444  vmadivsumb  27446  rpvmasumlem  27450  dchrisum0re  27476  dchrisum0  27483  selberg2b  27515  selberg3lem2  27521  pntrsumbnd  27529  pntrlog2bnd  27547  nocvxmin  27747  mulsgt0  28136  nnaddscl  28338  nnmulscl  28339  ishpg  28827  axcontlem2  29034  umgr2edg  29278  umgrvad2edg  29282  uhgrspan1  29372  wlkeq  29702  clwwlkccatlem  30059  wwlksext2clwwlk  30127  conngrv2edg  30265  frgrnbnb  30363  frgrwopreglem5lem  30390  frgrwopreglem5ALT  30392  grporcan  30589  blocni  30876  ubthlem3  30943  htthlem  30988  hvsub4  31108  shscli  31388  elspansn4  31644  5oalem2  31726  hosub4  31884  hmops  32091  hmopco  32094  adjadd  32164  hstpyth  32300  hstles  32302  mdsl0  32381  mdslmd1lem2  32397  chirredlem1  32461  chirredlem2  32462  chirredlem3  32463  chirredlem4  32464  mdsymlem6  32479  cdj3lem2b  32508  1stpreimas  32779  irngnzply1  33835  mdetpmtr2  33968  esumpcvgval  34222  signstfvc  34718  noinfepfnregs  35276  satffunlem  35583  mpomulnzcnf  36481  tailfb  36559  isbasisrelowllem1  37671  isbasisrelowllem2  37672  poimirlem14  37955  heicant  37976  mblfinlem4  37981  ismblfin  37982  itg2addnc  37995  ftc1cnnc  38013  filbcmb  38061  prdsbnd  38114  ismtyval  38121  heiborlem8  38139  ghomco  38212  mzpindd  43178  tfsconcatun  43765  oaun3lem1  43802  oaun3lem2  43803  mulltgt0  45453  stoweidlem46  46474  fourierdlem73  46607  cfsetsnfsetf1  47507  iccelpart  47893  bgoldbtbnd  48285  grimco  48365  isubgrgrim  48405  usgrgrtrirex  48426  grlictr  48491  2zrngmmgm  48728  srhmsubcALTV  48801  zlmodzxzsubm  48835  zlmodzxzsub  48836