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  4113  reupick3  4293  difprsnss  4763  opthhausdorff  5477  pwssun  5530  trin2  6096  sspred  6283  fundif  6565  fnun  6632  f1cof1  6766  f1oun  6819  f1oco  6823  eqfnfv  7003  eqfunfv  7008  sorpsscmpl  7710  ordsucsssuc  7798  ordsucun  7800  resf1extb  7910  soxp  8108  poseq  8137  ressuppssdif  8164  frrlem4  8268  issmo  8317  tfrlem5  8348  ener  8972  domtr  8978  unen  9017  xpdom2  9036  mapen  9105  unxpdomlem3  9199  fiin  9373  suc11reg  9572  djuunxp  9874  xpnum  9904  pm54.43  9954  r0weon  9965  fseqen  9980  kmlem9  10112  axpre-lttrn  11119  axpre-mulgt0  11121  wloglei  11710  mulnzcnf  11824  zaddcl  12573  zmulcl  12582  qaddcl  12924  qmulcl  12926  rpaddcl  12975  rpmulcl  12976  rpdivcl  12978  xrltnsym  13097  xrlttri  13099  xmullem  13224  xmulcom  13226  xmulneg1  13229  xmulf  13232  ge0addcl  13421  ge0mulcl  13422  ge0xaddcl  13423  ge0xmulcl  13424  serge0  14021  expclzlem  14048  expge0  14063  expge1  14064  hashfacen  14419  wwlktovf1  14923  nn0rppwr  16531  nn0expgcd  16534  qredeu  16628  nn0gcdsq  16722  mul4sq  16925  fpwipodrs  18499  pwmnd  18864  gimco  19200  gictr  19208  symgextf1  19351  efgrelexlemb  19680  xrs1mnd  21321  pzriprnglem5  21395  pzriprnglem8  21398  lmimco  21753  lmictra  21754  cctop  22893  iscn2  23125  iscnp2  23126  paste  23181  txuni  23479  txcn  23513  txcmpb  23531  tx2ndc  23538  hmphtr  23670  snfil  23751  supfil  23782  filssufilg  23798  tsmsxp  24042  dscmet  24460  rlimcnp  26875  efnnfsumcl  27013  efchtdvds  27069  lgsne0  27246  mul2sq  27330  sltsolem1  27587  ssltsn  27704  colinearalglem2  28834  nb3grprlem2  29308  cplgr3v  29362  crctcshwlkn0  29751  wwlksnextinj  29829  hsn0elch  31177  shscli  31246  hsupss  31270  5oalem6  31588  mdsldmd1i  32260  superpos  32283  bnj110  34848  msubco  35518  fnsingle  35907  funimage  35916  funpartfun  35931  mpomulnzcnf  36287  bj-nnfan  36736  bj-nnfor  36738  bj-snsetex  36951  bj-snmoore  37101  difunieq  37362  riscer  37982  divrngidl  38022  dvdsexpnn0  42322  zaddcom  42452  zmulcom  42456  rimco  42506  rictr  42508  mzpincl  42722  kelac2lem  43053  omcl3g  43323  cllem0  43555  unhe1  43774  permaxun  45001  tz6.12-1-afv  47175  tz6.12-1-afv2  47242  sprsymrelf1  47497  prmdvdsfmtnof1lem2  47586  grictr  47923  usgrexmpl2trifr  48028  gpgprismgr4cycllem7  48091  uspgrsprf1  48135  2zrngamgm  48233  2zrngmmgm  48240  rrx2xpref1o  48707  f1omoOLD  48882