Theorem ad2ant2r 783

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  disjxiun  4649  fundif  5935  funcnvqp  5952  foco  6125  fliftfun  6562  wfr3g  7413  omordi  7646  f1imaen2g  8017  isinf  8173  frfi  8205  acndom2  8877  infxp  9037  cff1  9080  isf32lem7  9181  fpwwe2lem12  9463  inawinalem  9511  inar1  9597  grur1  9642  genpnnp  9827  ltexprlem7  9864  prlem936  9869  reclem3pr  9871  1re  10039  addsub4  10324  muladd  10462  lt2add  10513  mullt0  10547  mulnzcnopr  10673  divmuldiv  10725  divmul24  10729  divmuleq  10730  recdiv  10731  divadddiv  10740  conjmul  10742  prodgt0  10868  ltmul12a  10879  lemul12b  10880  lediv12a  10916  lediv2a  10917  qmulcl  11806  irrmul  11813  xrrege0  12005  xmulge0  12114  ge0addcl  12284  ge0mulcl  12285  ge0xaddcl  12286  ge0xmulcl  12287  fzass4  12379  fzrev  12403  fzocatel  12531  serge0  12855  expclzlem  12884  expge0  12896  expge1  12897  lt2sq  12937  le2sq  12938  bernneq  12990  ccatw2s1p1  13413  ccatw2s1p2  13414  cshwleneq  13563  s2eq2seq  13682  sqrmo  13992  limsupval2  14211  o1lo12  14269  climrlim2  14278  2clim  14303  climsup  14400  tanaddlem  14896  opeo  15089  omeo  15090  divalglem8  15123  coprmproddvdslem  15376  pcpremul  15548  pcmul  15556  setscom  15903  fpwipodrs  17164  dfgrp3lem  17513  grplactcnv  17518  resgrpisgrp  17615  ghmpreima  17682  ghmeql  17683  conjghm  17691  pgpfi  18020  lmodprop2d  18925  lidlmcl  19217  xrs1mnd  19784  absabv  19803  frlmipval  20118  lmimco  20183  mavmulass  20355  mdetdiaglem  20404  cramerimplem2  20490  opnneissb  20918  cncnpi  21082  pnrmopn  21147  cmpsub  21203  connsub  21224  t1connperf  21239  neitx  21410  txcnmpt  21427  txrest  21434  txdis1cn  21438  tx1stc  21453  qtopcn  21517  trfg  21695  rnelfmlem  21756  flffbas  21799  nmo0  22539  nmoid  22546  cfilfcls  23072  iscmet3lem2  23090  caubl  23106  relcmpcmet  23115  ovolun  23267  ovolicc2lem3  23287  volsup  23324  ioombl1lem4  23329  ismbf3d  23421  mbfimaopnlem  23422  i1faddlem  23460  itgle  23576  ellimc2  23641  ftc1a  23800  dgrmul  24026  itgulm  24162  abelthlem8  24193  ptolemy  24248  logdivlt  24367  cxplt3  24446  cxple3  24447  o1cxp  24701  basellem4  24810  sqf11  24865  lgslem3  25024  lgsdir2  25055  lgsne0  25060  lgsquad3  25112  chpo1ubb  25170  vmadivsumb  25172  rpvmasumlem  25176  dchrisum0re  25202  dchrisum0  25209  selberg2b  25241  selberg3lem2  25247  pntrsumbnd  25255  pntrlog2bnd  25273  axcontlem2  25845  umgr2edg  26101  umgrvad2edg  26105  uhgrspan1  26195  wlkeq  26529  wwlksext2clwwlk  26924  conngrv2edg  27055  frgrnbnb  27157  frgrwopreglem5lem  27184  frgrwopreglem5ALT  27186  grporcan  27372  blocni  27660  ubthlem3  27728  htthlem  27774  hvsub4  27894  shscli  28176  elspansn4  28432  5oalem2  28514  hosub4  28672  hmops  28879  hmopco  28882  adjadd  28952  hstpyth  29088  hstles  29090  mdsl0  29169  mdslmd1lem2  29185  chirredlem1  29249  chirredlem2  29250  chirredlem3  29251  chirredlem4  29252  mdsymlem6  29267  cdj3lem2b  29296  1stpreimas  29483  mdetpmtr2  29890  esumpcvgval  30140  frr3g  31779  nocvxmin  31894  tailfb  32372  isbasisrelowllem1  33203  isbasisrelowllem2  33204  poimirlem14  33423  heicant  33444  mblfinlem4  33449  ismblfin  33450  itg2addnc  33464  ftc1cnnc  33484  filbcmb  33535  prdsbnd  33592  ismtyval  33599  heiborlem8  33617  ghomco  33690  mzpindd  37309  rp-fakenanass  37860  mulltgt0  39181  stoweidlem46  40263  fourierdlem73  40396  iccelpart  41369  bgoldbtbnd  41697  2zrngmmgm  41946  srhmsubc  42076  srhmsubcALTV  42094  zlmodzxzsubm  42137  zlmodzxzsub  42138