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  5104  fundif  6565  funcnvqp  6580  fliftfun  7287  wfr3g  8298  omordi  8530  nadd4  8662  naddel12  8664  f1imaen2g  8986  isinf  9207  isinfOLD  9208  frfi  9232  frr3g  9709  acndom2  10007  infxp  10167  cff1  10211  isf32lem7  10312  fpwwe2lem11  10594  inawinalem  10642  inar1  10728  grur1  10773  genpnnp  10958  ltexprlem7  10995  prlem936  11000  reclem3pr  11002  1re  11174  addsub4  11465  muladd  11610  lt2add  11663  mullt0  11697  mulnzcnf  11824  divmuldiv  11882  divmul24  11886  divmuleq  11887  recdiv  11888  divadddiv  11897  conjmul  11899  prodgt0  12029  ltmul12a  12038  lemul12b  12039  lediv12a  12076  lediv2a  12077  qmulcl  12926  irrmul  12933  xrrege0  13134  xmulge0  13244  ge0addcl  13421  ge0mulcl  13422  ge0xaddcl  13423  ge0xmulcl  13424  fzass4  13523  fzrev  13548  fzocatel  13690  serge0  14021  expclzlem  14048  expge0  14063  expge1  14064  lt2sq  14098  le2sq  14099  bernneq  14194  ccatw2s1p2  14602  swrdccatin2  14694  cshwleneq  14782  s2eq2seq  14903  wwlktovf1  14923  sqrmo  15217  limsupval2  15446  o1lo12  15504  climrlim2  15513  2clim  15538  climsup  15636  tanaddlem  16134  opeo  16335  omeo  16336  divalglem8  16370  coprmproddvdslem  16632  pcpremul  16814  pcmul  16822  setscom  17150  fpwipodrs  18499  gsumsgrpccat  18767  dfgrp3lem  18970  grplactcnv  18975  resgrpisgrp  19079  ghmpreima  19170  ghmeql  19171  conjghm  19181  pgpfi  19535  rngpropd  20083  srhmsubc  20589  lmodprop2d  20830  cndrng  21310  xrs1mnd  21321  absabv  21341  frlmipval  21688  lmimco  21753  mavmulass  22436  mdetdiaglem  22485  cramerimplem2  22571  opnneissb  23001  cncnpi  23165  pnrmopn  23230  cmpsub  23287  connsub  23308  t1connperf  23323  neitx  23494  txcnmpt  23511  txrest  23518  txdis1cn  23522  tx1stc  23537  qtopcn  23601  trfg  23778  rnelfmlem  23839  flffbas  23882  nmo0  24623  nmoid  24630  cfilfcls  25174  iscmet3lem2  25192  caubl  25208  relcmpcmet  25218  ovolun  25400  ovolicc2lem3  25420  volsup  25457  ioombl1lem4  25462  ismbf3d  25555  mbfimaopnlem  25556  i1faddlem  25594  itgle  25711  ellimc2  25778  ftc1a  25944  dgrmul  26176  itgulm  26317  abelthlem8  26349  ptolemy  26405  logdivlt  26530  cxplt3  26609  cxple3  26610  o1cxp  26885  basellem4  26994  sqf11  27049  lgslem3  27210  lgsdir2  27241  lgsne0  27246  lgsquad3  27298  chpo1ubb  27392  vmadivsumb  27394  rpvmasumlem  27398  dchrisum0re  27424  dchrisum0  27431  selberg2b  27463  selberg3lem2  27469  pntrsumbnd  27477  pntrlog2bnd  27495  nocvxmin  27690  mulsgt0  28047  nnaddscl  28238  nnmulscl  28239  ishpg  28686  axcontlem2  28892  umgr2edg  29136  umgrvad2edg  29140  uhgrspan1  29230  wlkeq  29562  clwwlkccatlem  29918  wwlksext2clwwlk  29986  conngrv2edg  30124  frgrnbnb  30222  frgrwopreglem5lem  30249  frgrwopreglem5ALT  30251  grporcan  30447  blocni  30734  ubthlem3  30801  htthlem  30846  hvsub4  30966  shscli  31246  elspansn4  31502  5oalem2  31584  hosub4  31742  hmops  31949  hmopco  31952  adjadd  32022  hstpyth  32158  hstles  32160  mdsl0  32239  mdslmd1lem2  32255  chirredlem1  32319  chirredlem2  32320  chirredlem3  32321  chirredlem4  32322  mdsymlem6  32337  cdj3lem2b  32366  1stpreimas  32629  irngnzply1  33686  mdetpmtr2  33814  esumpcvgval  34068  signstfvc  34565  satffunlem  35388  mpomulnzcnf  36287  tailfb  36365  isbasisrelowllem1  37343  isbasisrelowllem2  37344  poimirlem14  37628  heicant  37649  mblfinlem4  37654  ismblfin  37655  itg2addnc  37668  ftc1cnnc  37686  filbcmb  37734  prdsbnd  37787  ismtyval  37794  heiborlem8  37812  ghomco  37885  mzpindd  42734  tfsconcatun  43326  oaun3lem1  43363  oaun3lem2  43364  mulltgt0  45016  stoweidlem46  46044  fourierdlem73  46177  cfsetsnfsetf1  47060  iccelpart  47434  bgoldbtbnd  47810  grimco  47889  isubgrgrim  47929  usgrgrtrirex  47949  grlictr  48007  2zrngmmgm  48240  srhmsubcALTV  48313  zlmodzxzsubm  48347  zlmodzxzsub  48348