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  5100  fundif  6583  funcnvqp  6598  xpsntpg  7138  fliftfun  7314  wfr3g  8319  omordi  8554  nadd4  8688  naddel12  8690  f1imaen2g  9022  isinf  9236  frfi  9256  frr3g  9739  acndom2  10058  infxp  10217  cff1  10261  isf32lem7  10362  fpwwe2lem11  10651  inawinalem  10699  inar1  10785  grur1  10830  genpnnp  11015  ltexprlem7  11052  prlem936  11057  reclem3pr  11059  1re  11233  addsub4  11526  muladd  11671  lt2add  11724  mullt0  11758  mulnzcnf  11885  divmuldiv  11940  divmul24  11944  divmuleq  11945  recdiv  11946  divadddiv  11955  conjmul  11957  prodgt0  12087  ltmul12a  12096  lemul12b  12097  lediv12a  12133  lediv2a  12134  qmulcl  13018  irrmul  13025  xrrege0  13227  xmulge0  13337  ge0addcl  13514  ge0mulcl  13515  ge0xaddcl  13516  ge0xmulcl  13517  fzass4  13618  fzrev  13643  fzocatel  13786  serge0  14121  expclzlem  14148  expge0  14163  expge1  14164  lt2sq  14198  le2sq  14199  bernneq  14294  ccatw2s1p2  14706  swrdccatin2  14799  cshwleneq  14889  s2eq2seq  15009  wwlktovf1  15031  sqrmo  15339  limsupval2  15568  o1lo12  15626  climrlim2  15635  2clim  15660  climsup  15758  tanaddlem  16255  opeo  16456  omeo  16457  divalglem8  16491  coprmproddvdslem  16753  pcpremul  16936  pcmul  16944  setscom  17273  fpwipodrs  18629  gsumsgrpccat  18950  dfgrp3lem  19162  grplactcnv  19167  resgrpisgrp  19272  ghmpreima  19366  ghmeql  19367  conjghm  19377  pgpfi  19733  rngpropd  20310  srhmsubc  20843  lmodprop2d  21109  cndrng  21615  absabv  21638  xrs1mnd  21654  frlmipval  21993  lmimco  22058  mavmulass  22772  mdetdiaglem  22821  cramerimplem2  22910  opnneissb  23340  cncnpi  23504  pnrmopn  23569  cmpsub  23626  connsub  23647  t1connperf  23662  neitx  23834  txcnmpt  23851  txrest  23858  txdis1cn  23862  tx1stc  23877  qtopcn  23941  trfg  24118  rnelfmlem  24179  flffbas  24222  nmo0  24962  nmoid  24969  cfilfcls  25503  iscmet3lem2  25521  caubl  25537  relcmpcmet  25547  ovolun  25728  ovolicc2lem3  25748  volsup  25785  ioombl1lem4  25790  ismbf3d  25883  mbfimaopnlem  25884  i1faddlem  25922  itgle  26038  ellimc2  26105  ftc1a  26265  dgrmul  26497  itgulm  26645  abelthlem8  26676  ptolemy  26735  logdivlt  26859  cxplt3  26938  cxple3  26939  o1cxp  27212  basellem4  27321  sqf11  27376  lgslem3  27536  lgsdir2  27567  lgsne0  27572  lgsquad3  27624  chpo1ubb  27718  vmadivsumb  27720  rpvmasumlem  27724  dchrisum0re  27750  dchrisum0  27757  selberg2b  27789  selberg3lem2  27795  pntrsumbnd  27803  pntrlog2bnd  27821  nocvxmin  28021  mulsgt0  28410  nnaddscl  28612  nnmulscl  28613  ishpg  29117  axcontlem2  29423  umgr2edg  29670  umgrvad2edg  29674  uhgrspan1  29764  wlkeq  30094  clwwlkccatlem  30460  wwlksext2clwwlk  30528  conngrv2edg  30676  frgrnbnb  30774  frgrwopreglem5lem  30801  frgrwopreglem5ALT  30803  grporcan  31000  blocni  31287  ubthlem3  31354  htthlem  31399  hvsub4  31519  shscli  31799  elspansn4  32055  5oalem2  32137  hosub4  32295  hmops  32502  hmopco  32505  adjadd  32575  hstpyth  32711  hstles  32713  mdsl0  32792  mdslmd1lem2  32808  chirredlem1  32872  chirredlem2  32873  chirredlem3  32874  chirredlem4  32875  mdsymlem6  32890  cdj3lem2b  32919  1stpreimas  33179  irngnzply1  34202  mdetpmtr2  34335  esumpcvgval  34589  signstfvc  35083  noinfepfnregs  35659  satffunlem  35981  nmulprop  36771  nmulel1  36796  mpomulnzcnf  36920  tailfb  36997  isbasisrelowllem1  38110  isbasisrelowllem2  38111  poimirlem14  38384  heicant  38405  mblfinlem4  38410  ismblfin  38411  itg2addnc  38424  ftc1cnnc  38442  filbcmb  38491  prdsbnd  38544  ismtyval  38551  heiborlem8  38569  ghomco  38642  mzpindd  43592  tfsconcatun  44179  oaun3lem1  44216  oaun3lem2  44217  mulltgt0  45857  stoweidlem46  46875  fourierdlem73  47008  cfsetsnfsetf1  47948  iccelpart  48334  bgoldbtbnd  48726  grimco  48806  isubgrgrim  48846  usgrgrtrirex  48867  grlictr  48932  2zrngmmgm  49168  srhmsubcALTV  49241  zlmodzxzsubm  49290  zlmodzxzsub  49291