Theorem syl2anb 598

Description: A double syllogism inference. (Contributed by NM, 29-Jul-1999.)

Hypotheses

Ref	Expression
syl2anb.1	⊢ (𝜑 ↔ 𝜓)
syl2anb.2	⊢ (𝜏 ↔ 𝜒)
syl2anb.3	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
syl2anb	⊢ ((𝜑 ∧ 𝜏) → 𝜃)

Proof of Theorem syl2anb

Step	Hyp	Ref	Expression
1		syl2anb.2	. 2 ⊢ (𝜏 ↔ 𝜒)
2		syl2anb.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3		syl2anb.3	. . 3 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylanb 581	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	sylan2b 594	1 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 206   ∧ 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:  sylancb  600  rexdifi  4150  reupick3  4330  difprsnss  4799  opthhausdorff  5522  pwssun  5575  trin2  6143  sspred  6330  fundif  6615  fnun  6682  f1cof1  6814  f1oun  6867  f1oco  6871  eqfnfv  7051  eqfunfv  7056  sorpsscmpl  7754  ordsucsssuc  7843  ordsucun  7845  resf1extb  7956  soxp  8154  poseq  8183  ressuppssdif  8210  frrlem4  8314  wfrlem4OLD  8352  issmo  8388  tfrlem5  8420  ener  9041  domtr  9047  unen  9086  xpdom2  9107  mapen  9181  unxpdomlem3  9288  fiin  9462  suc11reg  9659  djuunxp  9961  xpnum  9991  pm54.43  10041  r0weon  10052  fseqen  10067  kmlem9  10199  axpre-lttrn  11206  axpre-mulgt0  11208  wloglei  11795  mulnzcnf  11909  zaddcl  12657  zmulcl  12666  qaddcl  13007  qmulcl  13009  rpaddcl  13057  rpmulcl  13058  rpdivcl  13060  xrltnsym  13179  xrlttri  13181  xmullem  13306  xmulcom  13308  xmulneg1  13311  xmulf  13314  ge0addcl  13500  ge0mulcl  13501  ge0xaddcl  13502  ge0xmulcl  13503  serge0  14097  expclzlem  14124  expge0  14139  expge1  14140  hashfacen  14493  wwlktovf1  14996  nn0rppwr  16598  nn0expgcd  16601  qredeu  16695  nn0gcdsq  16789  mul4sq  16992  fpwipodrs  18585  pwmnd  18950  gimco  19286  gictr  19294  symgextf1  19439  efgrelexlemb  19768  xrs1mnd  21422  pzriprnglem5  21496  pzriprnglem8  21499  lmimco  21864  lmictra  21865  cctop  23013  iscn2  23246  iscnp2  23247  paste  23302  txuni  23600  txcn  23634  txcmpb  23652  tx2ndc  23659  hmphtr  23791  snfil  23872  supfil  23903  filssufilg  23919  tsmsxp  24163  dscmet  24585  rlimcnp  27008  efnnfsumcl  27146  efchtdvds  27202  lgsne0  27379  mul2sq  27463  sltsolem1  27720  ssltsn  27837  nohalf  28407  colinearalglem2  28922  nb3grprlem2  29398  cplgr3v  29452  crctcshwlkn0  29841  wwlksnextinj  29919  hsn0elch  31267  shscli  31336  hsupss  31360  5oalem6  31678  mdsldmd1i  32350  superpos  32373  bnj110  34872  msubco  35536  fnsingle  35920  funimage  35929  funpartfun  35944  mpomulnzcnf  36300  bj-nnfan  36749  bj-nnfor  36751  bj-snsetex  36964  bj-snmoore  37114  difunieq  37375  riscer  37995  divrngidl  38035  dvdsexpnn0  42369  zaddcom  42482  zmulcom  42486  rimco  42528  rictr  42530  mzpincl  42745  kelac2lem  43076  omcl3g  43347  cllem0  43579  unhe1  43798  tz6.12-1-afv  47186  tz6.12-1-afv2  47253  sprsymrelf1  47483  prmdvdsfmtnof1lem2  47572  grictr  47892  usgrexmpl2trifr  47996  uspgrsprf1  48063  2zrngamgm  48161  2zrngmmgm  48168  rrx2xpref1o  48639  f1omo  48792