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  4099  reupick3  4279  difprsnss  4750  opthhausdorff  5460  pwssun  5511  trin2  6074  sspred  6262  fundif  6535  fnun  6600  f1cof1  6734  f1oun  6787  f1oco  6791  eqfnfv  6970  eqfunfv  6975  sorpsscmpl  7673  ordsucsssuc  7759  ordsucun  7761  resf1extb  7870  soxp  8065  poseq  8094  ressuppssdif  8121  frrlem4  8225  issmo  8274  tfrlem5  8305  ener  8930  domtr  8936  unen  8974  xpdom2  8992  mapen  9061  unxpdomlem3  9149  fiin  9313  suc11reg  9516  djuunxp  9821  xpnum  9851  pm54.43  9901  r0weon  9910  fseqen  9925  kmlem9  10057  axpre-lttrn  11064  axpre-mulgt0  11066  wloglei  11656  mulnzcnf  11770  zaddcl  12518  zmulcl  12527  qaddcl  12865  qmulcl  12867  rpaddcl  12916  rpmulcl  12917  rpdivcl  12919  xrltnsym  13038  xrlttri  13040  xmullem  13165  xmulcom  13167  xmulneg1  13170  xmulf  13173  ge0addcl  13362  ge0mulcl  13363  ge0xaddcl  13364  ge0xmulcl  13365  serge0  13965  expclzlem  13992  expge0  14007  expge1  14008  hashfacen  14363  wwlktovf1  14866  nn0rppwr  16474  nn0expgcd  16477  qredeu  16571  nn0gcdsq  16665  mul4sq  16868  fpwipodrs  18448  pwmnd  18847  gimco  19182  gictr  19190  symgextf1  19335  efgrelexlemb  19664  xrs1mnd  21379  pzriprnglem5  21424  pzriprnglem8  21427  lmimco  21783  lmictra  21784  cctop  22922  iscn2  23154  iscnp2  23155  paste  23210  txuni  23508  txcn  23542  txcmpb  23560  tx2ndc  23567  hmphtr  23699  snfil  23780  supfil  23811  filssufilg  23827  tsmsxp  24071  dscmet  24488  rlimcnp  26903  efnnfsumcl  27041  efchtdvds  27097  lgsne0  27274  mul2sq  27358  sltsolem1  27615  zs12addscl  28388  colinearalglem2  28887  nb3grprlem2  29361  cplgr3v  29415  crctcshwlkn0  29801  wwlksnextinj  29879  hsn0elch  31230  shscli  31299  hsupss  31323  5oalem6  31641  mdsldmd1i  32313  superpos  32336  bnj110  34891  msubco  35596  fnsingle  35982  funimage  35991  funpartfun  36008  mpomulnzcnf  36364  bj-nnfan  36813  bj-nnfor  36815  bj-snsetex  37028  bj-snmoore  37178  difunieq  37439  riscer  38048  divrngidl  38088  dvdsexpnn0  42452  zaddcom  42582  zmulcom  42586  rimco  42636  rictr  42638  mzpincl  42851  kelac2lem  43181  omcl3g  43451  cllem0  43683  unhe1  43902  permaxun  45128  tz6.12-1-afv  47298  tz6.12-1-afv2  47365  sprsymrelf1  47620  prmdvdsfmtnof1lem2  47709  grictr  48047  usgrexmpl2trifr  48161  gpgprismgr4cycllem7  48225  uspgrsprf1  48271  2zrngamgm  48369  2zrngmmgm  48376  rrx2xpref1o  48843  f1omoOLD  49018