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  4103  reupick3  4283  difprsnss  4753  opthhausdorff  5464  pwssun  5515  trin2  6076  sspred  6262  fundif  6535  fnun  6600  f1cof1  6734  f1oun  6787  f1oco  6791  eqfnfv  6969  eqfunfv  6974  sorpsscmpl  7674  ordsucsssuc  7762  ordsucun  7764  resf1extb  7874  soxp  8069  poseq  8098  ressuppssdif  8125  frrlem4  8229  issmo  8278  tfrlem5  8309  ener  8933  domtr  8939  unen  8978  xpdom2  8996  mapen  9065  unxpdomlem3  9157  fiin  9331  suc11reg  9534  djuunxp  9836  xpnum  9866  pm54.43  9916  r0weon  9925  fseqen  9940  kmlem9  10072  axpre-lttrn  11079  axpre-mulgt0  11081  wloglei  11670  mulnzcnf  11784  zaddcl  12533  zmulcl  12542  qaddcl  12884  qmulcl  12886  rpaddcl  12935  rpmulcl  12936  rpdivcl  12938  xrltnsym  13057  xrlttri  13059  xmullem  13184  xmulcom  13186  xmulneg1  13189  xmulf  13192  ge0addcl  13381  ge0mulcl  13382  ge0xaddcl  13383  ge0xmulcl  13384  serge0  13981  expclzlem  14008  expge0  14023  expge1  14024  hashfacen  14379  wwlktovf1  14882  nn0rppwr  16490  nn0expgcd  16493  qredeu  16587  nn0gcdsq  16681  mul4sq  16884  fpwipodrs  18464  pwmnd  18829  gimco  19165  gictr  19173  symgextf1  19318  efgrelexlemb  19647  xrs1mnd  21365  pzriprnglem5  21410  pzriprnglem8  21413  lmimco  21769  lmictra  21770  cctop  22909  iscn2  23141  iscnp2  23142  paste  23197  txuni  23495  txcn  23529  txcmpb  23547  tx2ndc  23554  hmphtr  23686  snfil  23767  supfil  23798  filssufilg  23814  tsmsxp  24058  dscmet  24476  rlimcnp  26891  efnnfsumcl  27029  efchtdvds  27085  lgsne0  27262  mul2sq  27346  sltsolem1  27603  ssltsn  27721  zs12addscl  28372  colinearalglem2  28870  nb3grprlem2  29344  cplgr3v  29398  crctcshwlkn0  29784  wwlksnextinj  29862  hsn0elch  31210  shscli  31279  hsupss  31303  5oalem6  31621  mdsldmd1i  32293  superpos  32316  bnj110  34824  msubco  35503  fnsingle  35892  funimage  35901  funpartfun  35916  mpomulnzcnf  36272  bj-nnfan  36721  bj-nnfor  36723  bj-snsetex  36936  bj-snmoore  37086  difunieq  37347  riscer  37967  divrngidl  38007  dvdsexpnn0  42307  zaddcom  42437  zmulcom  42441  rimco  42491  rictr  42493  mzpincl  42707  kelac2lem  43037  omcl3g  43307  cllem0  43539  unhe1  43758  permaxun  44985  tz6.12-1-afv  47159  tz6.12-1-afv2  47226  sprsymrelf1  47481  prmdvdsfmtnof1lem2  47570  grictr  47908  usgrexmpl2trifr  48022  gpgprismgr4cycllem7  48086  uspgrsprf1  48132  2zrngamgm  48230  2zrngmmgm  48237  rrx2xpref1o  48704  f1omoOLD  48879