Theorem syl2anb 599

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 582	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	sylan2b 595	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  601  rexdifi  4104  reupick3  4284  difprsnss  4757  opthhausdorff  5473  pwssun  5524  trin2  6088  sspred  6276  fundif  6549  fnun  6614  f1cof1  6748  f1oun  6801  f1oco  6805  eqfnfv  6985  eqfunfv  6990  sorpsscmpl  7689  ordsucsssuc  7775  ordsucun  7777  resf1extb  7886  soxp  8081  poseq  8110  ressuppssdif  8137  frrlem4  8241  issmo  8290  tfrlem5  8321  ener  8950  domtr  8956  unen  8994  xpdom2  9012  mapen  9081  unxpdomlem3  9170  fiin  9337  suc11reg  9540  djuunxp  9845  xpnum  9875  pm54.43  9925  r0weon  9934  fseqen  9949  kmlem9  10081  axpre-lttrn  11089  axpre-mulgt0  11091  wloglei  11681  mulnzcnf  11795  zaddcl  12543  zmulcl  12552  qaddcl  12890  qmulcl  12892  rpaddcl  12941  rpmulcl  12942  rpdivcl  12944  xrltnsym  13063  xrlttri  13065  xmullem  13191  xmulcom  13193  xmulneg1  13196  xmulf  13199  ge0addcl  13388  ge0mulcl  13389  ge0xaddcl  13390  ge0xmulcl  13391  serge0  13991  expclzlem  14018  expge0  14033  expge1  14034  hashfacen  14389  wwlktovf1  14892  nn0rppwr  16500  nn0expgcd  16503  qredeu  16597  nn0gcdsq  16691  mul4sq  16894  fpwipodrs  18475  pwmnd  18874  gimco  19209  gictr  19217  symgextf1  19362  efgrelexlemb  19691  xrs1mnd  21407  pzriprnglem5  21452  pzriprnglem8  21455  lmimco  21811  lmictra  21812  cctop  22962  iscn2  23194  iscnp2  23195  paste  23250  txuni  23548  txcn  23582  txcmpb  23600  tx2ndc  23607  hmphtr  23739  snfil  23820  supfil  23851  filssufilg  23867  tsmsxp  24111  dscmet  24528  rlimcnp  26943  efnnfsumcl  27081  efchtdvds  27137  lgsne0  27314  mul2sq  27398  ltssolem1  27655  z12addscl  28485  colinearalglem2  28992  nb3grprlem2  29466  cplgr3v  29520  crctcshwlkn0  29906  wwlksnextinj  29984  hsn0elch  31335  shscli  31404  hsupss  31428  5oalem6  31746  mdsldmd1i  32418  superpos  32441  bnj110  35033  msubco  35744  fnsingle  36130  funimage  36139  funpartfun  36156  mpomulnzcnf  36512  bj-nnfan  36989  bj-nnfor  36991  bj-snsetex  37205  bj-axseprep  37316  bj-snmoore  37360  difunieq  37623  riscer  38233  divrngidl  38273  dvdsexpnn0  42698  zaddcom  42828  zmulcom  42832  rimco  42882  rictr  42884  mzpincl  43085  kelac2lem  43415  omcl3g  43685  cllem0  43916  unhe1  44135  permaxun  45361  tz6.12-1-afv  47528  tz6.12-1-afv2  47595  sprsymrelf1  47850  prmdvdsfmtnof1lem2  47939  grictr  48277  usgrexmpl2trifr  48391  gpgprismgr4cycllem7  48455  uspgrsprf1  48501  2zrngamgm  48599  2zrngmmgm  48606  rrx2xpref1o  49072  f1omoOLD  49247