Theorem syl2anb 610

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 593	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	sylan2b 606	1 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sylancb  612  rexdifi  4089  reupick3  4278  difprsnss  4762  opthhausdorff  5494  pwssun  5547  trin2  6129  sspred  6331  fundifOLD  6611  fnun  6675  f1cof1  6812  f1oun  6866  f1oco  6870  eqfnfv  7052  eqfunfv  7058  sorpsscmpl  7774  ordsucsssuc  7858  ordsucun  7860  resf1extb  7970  soxp  8168  poseq  8202  ressuppssdif  8230  frrlem4  8335  issmo  8384  tfrlem5  8415  ener  9056  domtr  9062  unen  9101  xpdom2  9119  mapen  9188  unxpdomlem3  9277  fiin  9441  suc11reg  9647  djuunxp  10029  xpnum  10059  pm54.43  10109  r0weon  10118  fseqen  10133  kmlem9  10264  axpre-lttrn  11278  axpre-mulgt0  11280  wloglei  11875  mulnzcnf  11989  zaddcl  12763  zmulcl  12772  qaddcl  13120  qmulcl  13122  rpaddcl  13171  rpmulcl  13172  rpdivcl  13174  xrltnsym  13293  xrlttri  13295  xmullem  13421  xmulcom  13423  xmulneg1  13426  xmulf  13429  ge0addcl  13618  ge0mulcl  13619  ge0xaddcl  13620  ge0xmulcl  13621  serge0  14226  expclzlem  14253  expge0  14268  expge1  14269  hashfacen  14626  wwlktovf1  15139  nn0rppwr  16764  nn0expgcd  16767  qredeu  16862  nn0gcdsq  16957  mul4sq  17161  fpwipodrs  18743  pwmnd  19172  gimco  19511  gictr  19520  symgextf1  19665  efgrelexlemb  19994  rimco  20777  rictr  20782  xrs1mnd  21776  pzriprnglem5  21821  pzriprnglem8  21824  lmimco  22180  lmictra  22181  cctop  23354  iscn2  23586  iscnp2  23587  paste  23642  txuni  23941  txcn  23975  txcmpb  23993  tx2ndc  24000  hmphtr  24132  snfil  24213  supfil  24244  filssufilg  24260  tsmsxp  24504  dscmet  24921  rlimcnp  27323  efnnfsumcl  27460  efchtdvds  27516  lgsne0  27692  mul2sq  27776  ltssolem1  28062  z12addscl  28893  colinearalglem2  29515  nb3grprlem2  29992  cplgr3v  30046  crctcshwlkn0  30440  wwlksnextinj  30518  hsn0elch  31880  shscli  31949  hsupss  31973  5oalem6  32291  mdsldmd1i  32963  superpos  32986  bnj110  35558  scottsn  35834  msubco  36463  fnsingle  36859  funimage  36868  funpartfun  36885  mpomulnzcnf  37266  bj-nnfan  37834  bj-nnfor  37836  bj-snsetex  38054  bj-axseprep  38181  bj-snmoore  38225  difunieq  38489  riscer  39114  divrngidl  39154  dvdsexpnn0  43579  zaddcom  43721  zmulcom  43725  mzpincl  43938  kelac2lem  44259  omcl3g  44528  cllem0  44759  unhe1  44977  permaxun  46196  tz6.12-1-afv  48449  tz6.12-1-afv2  48516  sprsymrelf1  48783  prmdvdsfmtnof1lem2  48875  grictr  49226  usgrexmpl2trifr  49340  gpgprismgr4cycllem7  49404  uspgrsprf1  49450  2zrngamgm  49547  2zrngmmgm  49554  f1omoOLD  50213