Theorem ad2ant2r 744

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  disjxiun  5089  fundif  6533  funcnvqp  6548  fliftfun  7239  wfr3g  8208  omordi  8468  f1imaen2g  8876  isinf  9125  isinfOLD  9126  frfi  9153  frr3g  9613  acndom2  9911  infxp  10072  cff1  10115  isf32lem7  10216  fpwwe2lem11  10498  inawinalem  10546  inar1  10632  grur1  10677  genpnnp  10862  ltexprlem7  10899  prlem936  10904  reclem3pr  10906  1re  11076  addsub4  11365  muladd  11508  lt2add  11561  mullt0  11595  mulnzcnopr  11722  divmuldiv  11776  divmul24  11780  divmuleq  11781  recdiv  11782  divadddiv  11791  conjmul  11793  prodgt0  11923  ltmul12a  11932  lemul12b  11933  lediv12a  11969  lediv2a  11970  qmulcl  12808  irrmul  12815  xrrege0  13009  xmulge0  13119  ge0addcl  13293  ge0mulcl  13294  ge0xaddcl  13295  ge0xmulcl  13296  fzass4  13395  fzrev  13420  fzocatel  13552  serge0  13878  expclzlem  13907  expge0  13920  expge1  13921  lt2sq  13953  le2sq  13954  bernneq  14045  ccatw2s1p1OLD  14445  ccatw2s1p2  14446  swrdccatin2  14540  cshwleneq  14628  s2eq2seq  14749  wwlktovf1  14771  sqrmo  15062  limsupval2  15288  o1lo12  15346  climrlim2  15355  2clim  15380  climsup  15480  tanaddlem  15974  opeo  16173  omeo  16174  divalglem8  16208  coprmproddvdslem  16464  pcpremul  16641  pcmul  16649  setscom  16978  fpwipodrs  18355  gsumsgrpccat  18575  dfgrp3lem  18769  grplactcnv  18774  resgrpisgrp  18872  ghmpreima  18952  ghmeql  18953  conjghm  18961  pgpfi  19306  lmodprop2d  20291  lidlmcl  20594  xrs1mnd  20742  absabv  20761  frlmipval  21092  lmimco  21157  mavmulass  21804  mdetdiaglem  21853  cramerimplem2  21939  opnneissb  22371  cncnpi  22535  pnrmopn  22600  cmpsub  22657  connsub  22678  t1connperf  22693  neitx  22864  txcnmpt  22881  txrest  22888  txdis1cn  22892  tx1stc  22907  qtopcn  22971  trfg  23148  rnelfmlem  23209  flffbas  23252  nmo0  24005  nmoid  24012  cfilfcls  24544  iscmet3lem2  24562  caubl  24578  relcmpcmet  24588  ovolun  24769  ovolicc2lem3  24789  volsup  24826  ioombl1lem4  24831  ismbf3d  24924  mbfimaopnlem  24925  i1faddlem  24963  itgle  25080  ellimc2  25147  ftc1a  25307  dgrmul  25537  itgulm  25673  abelthlem8  25704  ptolemy  25759  logdivlt  25882  cxplt3  25961  cxple3  25962  o1cxp  26230  basellem4  26339  sqf11  26394  lgslem3  26553  lgsdir2  26584  lgsne0  26589  lgsquad3  26641  chpo1ubb  26735  vmadivsumb  26737  rpvmasumlem  26741  dchrisum0re  26767  dchrisum0  26774  selberg2b  26806  selberg3lem2  26812  pntrsumbnd  26820  pntrlog2bnd  26838  nocvxmin  27024  ishpg  27409  axcontlem2  27622  umgr2edg  27865  umgrvad2edg  27869  uhgrspan1  27959  wlkeq  28290  clwwlkccatlem  28641  wwlksext2clwwlk  28709  conngrv2edg  28847  frgrnbnb  28945  frgrwopreglem5lem  28972  frgrwopreglem5ALT  28974  grporcan  29168  blocni  29455  ubthlem3  29522  htthlem  29567  hvsub4  29687  shscli  29967  elspansn4  30223  5oalem2  30305  hosub4  30463  hmops  30670  hmopco  30673  adjadd  30743  hstpyth  30879  hstles  30881  mdsl0  30960  mdslmd1lem2  30976  chirredlem1  31040  chirredlem2  31041  chirredlem3  31042  chirredlem4  31043  mdsymlem6  31058  cdj3lem2b  31087  1stpreimas  31325  mdetpmtr2  32072  esumpcvgval  32344  signstfvc  32853  satffunlem  33662  tailfb  34662  isbasisrelowllem1  35631  isbasisrelowllem2  35632  poimirlem14  35896  heicant  35917  mblfinlem4  35922  ismblfin  35923  itg2addnc  35936  ftc1cnnc  35954  filbcmb  36003  prdsbnd  36056  ismtyval  36063  heiborlem8  36081  ghomco  36154  mzpindd  40830  mulltgt0  42886  stoweidlem46  43923  fourierdlem73  44056  cfsetsnfsetf1  44904  iccelpart  45236  bgoldbtbnd  45612  2zrngmmgm  45855  srhmsubc  45985  srhmsubcALTV  46003  zlmodzxzsubm  46046  zlmodzxzsub  46047