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  5099  fundif  6549  funcnvqp  6564  fliftfun  7269  wfr3g  8275  omordi  8507  nadd4  8639  naddel12  8641  f1imaen2g  8963  isinf  9183  isinfOLD  9184  frfi  9208  frr3g  9685  acndom2  9983  infxp  10143  cff1  10187  isf32lem7  10288  fpwwe2lem11  10570  inawinalem  10618  inar1  10704  grur1  10749  genpnnp  10934  ltexprlem7  10971  prlem936  10976  reclem3pr  10978  1re  11150  addsub4  11441  muladd  11586  lt2add  11639  mullt0  11673  mulnzcnf  11800  divmuldiv  11858  divmul24  11862  divmuleq  11863  recdiv  11864  divadddiv  11873  conjmul  11875  prodgt0  12005  ltmul12a  12014  lemul12b  12015  lediv12a  12052  lediv2a  12053  qmulcl  12902  irrmul  12909  xrrege0  13110  xmulge0  13220  ge0addcl  13397  ge0mulcl  13398  ge0xaddcl  13399  ge0xmulcl  13400  fzass4  13499  fzrev  13524  fzocatel  13666  serge0  13997  expclzlem  14024  expge0  14039  expge1  14040  lt2sq  14074  le2sq  14075  bernneq  14170  ccatw2s1p2  14578  swrdccatin2  14670  cshwleneq  14758  s2eq2seq  14879  wwlktovf1  14899  sqrmo  15193  limsupval2  15422  o1lo12  15480  climrlim2  15489  2clim  15514  climsup  15612  tanaddlem  16110  opeo  16311  omeo  16312  divalglem8  16346  coprmproddvdslem  16608  pcpremul  16790  pcmul  16798  setscom  17126  fpwipodrs  18481  gsumsgrpccat  18749  dfgrp3lem  18952  grplactcnv  18957  resgrpisgrp  19061  ghmpreima  19152  ghmeql  19153  conjghm  19163  pgpfi  19519  rngpropd  20094  srhmsubc  20600  lmodprop2d  20862  cndrng  21340  absabv  21366  xrs1mnd  21382  frlmipval  21721  lmimco  21786  mavmulass  22469  mdetdiaglem  22518  cramerimplem2  22604  opnneissb  23034  cncnpi  23198  pnrmopn  23263  cmpsub  23320  connsub  23341  t1connperf  23356  neitx  23527  txcnmpt  23544  txrest  23551  txdis1cn  23555  tx1stc  23570  qtopcn  23634  trfg  23811  rnelfmlem  23872  flffbas  23915  nmo0  24656  nmoid  24663  cfilfcls  25207  iscmet3lem2  25225  caubl  25241  relcmpcmet  25251  ovolun  25433  ovolicc2lem3  25453  volsup  25490  ioombl1lem4  25495  ismbf3d  25588  mbfimaopnlem  25589  i1faddlem  25627  itgle  25744  ellimc2  25811  ftc1a  25977  dgrmul  26209  itgulm  26350  abelthlem8  26382  ptolemy  26438  logdivlt  26563  cxplt3  26642  cxple3  26643  o1cxp  26918  basellem4  27027  sqf11  27082  lgslem3  27243  lgsdir2  27274  lgsne0  27279  lgsquad3  27331  chpo1ubb  27425  vmadivsumb  27427  rpvmasumlem  27431  dchrisum0re  27457  dchrisum0  27464  selberg2b  27496  selberg3lem2  27502  pntrsumbnd  27510  pntrlog2bnd  27528  nocvxmin  27724  mulsgt0  28087  nnaddscl  28278  nnmulscl  28279  ishpg  28739  axcontlem2  28945  umgr2edg  29189  umgrvad2edg  29193  uhgrspan1  29283  wlkeq  29614  clwwlkccatlem  29968  wwlksext2clwwlk  30036  conngrv2edg  30174  frgrnbnb  30272  frgrwopreglem5lem  30299  frgrwopreglem5ALT  30301  grporcan  30497  blocni  30784  ubthlem3  30851  htthlem  30896  hvsub4  31016  shscli  31296  elspansn4  31552  5oalem2  31634  hosub4  31792  hmops  31999  hmopco  32002  adjadd  32072  hstpyth  32208  hstles  32210  mdsl0  32289  mdslmd1lem2  32305  chirredlem1  32369  chirredlem2  32370  chirredlem3  32371  chirredlem4  32372  mdsymlem6  32387  cdj3lem2b  32416  1stpreimas  32679  irngnzply1  33679  mdetpmtr2  33807  esumpcvgval  34061  signstfvc  34558  satffunlem  35381  mpomulnzcnf  36280  tailfb  36358  isbasisrelowllem1  37336  isbasisrelowllem2  37337  poimirlem14  37621  heicant  37642  mblfinlem4  37647  ismblfin  37648  itg2addnc  37661  ftc1cnnc  37679  filbcmb  37727  prdsbnd  37780  ismtyval  37787  heiborlem8  37805  ghomco  37878  mzpindd  42727  tfsconcatun  43319  oaun3lem1  43356  oaun3lem2  43357  mulltgt0  45009  stoweidlem46  46037  fourierdlem73  46170  cfsetsnfsetf1  47053  iccelpart  47427  bgoldbtbnd  47803  grimco  47882  isubgrgrim  47922  usgrgrtrirex  47942  grlictr  48000  2zrngmmgm  48233  srhmsubcALTV  48306  zlmodzxzsubm  48340  zlmodzxzsub  48341