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  4090  reupick3  4270  difprsnss  4744  opthhausdorff  5471  pwssun  5523  trin2  6086  sspred  6274  fundif  6547  fnun  6612  f1cof1  6746  f1oun  6799  f1oco  6803  eqfnfv  6983  eqfunfv  6988  sorpsscmpl  7688  ordsucsssuc  7774  ordsucun  7776  resf1extb  7885  soxp  8079  poseq  8108  ressuppssdif  8135  frrlem4  8239  issmo  8288  tfrlem5  8319  ener  8948  domtr  8954  unen  8992  xpdom2  9010  mapen  9079  unxpdomlem3  9168  fiin  9335  suc11reg  9540  djuunxp  9845  xpnum  9875  pm54.43  9925  r0weon  9934  fseqen  9949  kmlem9  10081  axpre-lttrn  11089  axpre-mulgt0  11091  wloglei  11682  mulnzcnf  11796  zaddcl  12567  zmulcl  12576  qaddcl  12915  qmulcl  12917  rpaddcl  12966  rpmulcl  12967  rpdivcl  12969  xrltnsym  13088  xrlttri  13090  xmullem  13216  xmulcom  13218  xmulneg1  13221  xmulf  13224  ge0addcl  13413  ge0mulcl  13414  ge0xaddcl  13415  ge0xmulcl  13416  serge0  14018  expclzlem  14045  expge0  14060  expge1  14061  hashfacen  14416  wwlktovf1  14919  nn0rppwr  16530  nn0expgcd  16533  qredeu  16627  nn0gcdsq  16722  mul4sq  16925  fpwipodrs  18506  pwmnd  18908  gimco  19243  gictr  19251  symgextf1  19396  efgrelexlemb  19725  xrs1mnd  21420  pzriprnglem5  21465  pzriprnglem8  21468  lmimco  21824  lmictra  21825  cctop  22971  iscn2  23203  iscnp2  23204  paste  23259  txuni  23557  txcn  23591  txcmpb  23609  tx2ndc  23616  hmphtr  23748  snfil  23829  supfil  23860  filssufilg  23876  tsmsxp  24120  dscmet  24537  rlimcnp  26929  efnnfsumcl  27066  efchtdvds  27122  lgsne0  27298  mul2sq  27382  ltssolem1  27639  z12addscl  28469  colinearalglem2  28976  nb3grprlem2  29450  cplgr3v  29504  crctcshwlkn0  29889  wwlksnextinj  29967  hsn0elch  31319  shscli  31388  hsupss  31412  5oalem6  31730  mdsldmd1i  32402  superpos  32425  bnj110  35000  msubco  35713  fnsingle  36099  funimage  36108  funpartfun  36125  mpomulnzcnf  36481  bj-nnfan  37051  bj-nnfor  37053  bj-snsetex  37270  bj-axseprep  37381  bj-snmoore  37425  difunieq  37690  riscer  38309  divrngidl  38349  dvdsexpnn0  42766  zaddcom  42909  zmulcom  42913  rimco  42963  rictr  42965  mzpincl  43166  kelac2lem  43492  omcl3g  43762  cllem0  43993  unhe1  44212  permaxun  45438  tz6.12-1-afv  47622  tz6.12-1-afv2  47689  sprsymrelf1  47956  prmdvdsfmtnof1lem2  48048  grictr  48399  usgrexmpl2trifr  48513  gpgprismgr4cycllem7  48577  uspgrsprf1  48623  2zrngamgm  48721  2zrngmmgm  48728  rrx2xpref1o  49194  f1omoOLD  49369