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  4160  reupick3  4336  difprsnss  4804  opthhausdorff  5527  pwssun  5580  trin2  6146  sspred  6332  fundif  6617  fnun  6683  f1cof1  6815  f1oun  6868  f1oco  6872  eqfnfv  7051  eqfunfv  7056  sorpsscmpl  7753  ordsucsssuc  7843  ordsucun  7845  soxp  8153  poseq  8182  ressuppssdif  8209  frrlem4  8313  wfrlem4OLD  8351  issmo  8387  tfrlem5  8419  ener  9040  domtr  9046  unen  9085  xpdom2  9106  mapen  9180  unxpdomlem3  9286  fiin  9460  suc11reg  9657  djuunxp  9959  xpnum  9989  pm54.43  10039  r0weon  10050  fseqen  10065  kmlem9  10197  axpre-lttrn  11204  axpre-mulgt0  11206  wloglei  11793  mulnzcnf  11907  zaddcl  12655  zmulcl  12664  qaddcl  13005  qmulcl  13007  rpaddcl  13055  rpmulcl  13056  rpdivcl  13058  xrltnsym  13176  xrlttri  13178  xmullem  13303  xmulcom  13305  xmulneg1  13308  xmulf  13311  ge0addcl  13497  ge0mulcl  13498  ge0xaddcl  13499  ge0xmulcl  13500  serge0  14094  expclzlem  14121  expge0  14136  expge1  14137  hashfacen  14490  wwlktovf1  14993  nn0rppwr  16595  nn0expgcd  16598  qredeu  16692  nn0gcdsq  16786  mul4sq  16988  fpwipodrs  18598  pwmnd  18963  gimco  19299  gictr  19307  symgextf1  19454  efgrelexlemb  19783  xrs1mnd  21440  pzriprnglem5  21514  pzriprnglem8  21517  lmimco  21882  lmictra  21883  cctop  23029  iscn2  23262  iscnp2  23263  paste  23318  txuni  23616  txcn  23650  txcmpb  23668  tx2ndc  23675  hmphtr  23807  snfil  23888  supfil  23919  filssufilg  23935  tsmsxp  24179  dscmet  24601  rlimcnp  27023  efnnfsumcl  27161  efchtdvds  27217  lgsne0  27394  mul2sq  27478  sltsolem1  27735  ssltsn  27852  nohalf  28422  colinearalglem2  28937  nb3grprlem2  29413  cplgr3v  29467  crctcshwlkn0  29851  wwlksnextinj  29929  hsn0elch  31277  shscli  31346  hsupss  31370  5oalem6  31688  mdsldmd1i  32360  superpos  32383  bnj110  34851  msubco  35516  fnsingle  35901  funimage  35910  funpartfun  35925  mpomulnzcnf  36282  bj-nnfan  36731  bj-nnfor  36733  bj-snsetex  36946  bj-snmoore  37096  difunieq  37357  riscer  37975  divrngidl  38015  dvdsexpnn0  42348  zaddcom  42459  zmulcom  42463  rimco  42505  rictr  42507  mzpincl  42722  kelac2lem  43053  omcl3g  43324  cllem0  43556  unhe1  43775  tz6.12-1-afv  47124  tz6.12-1-afv2  47191  sprsymrelf1  47421  prmdvdsfmtnof1lem2  47510  grictr  47830  usgrexmpl2trifr  47932  uspgrsprf1  47991  2zrngamgm  48089  2zrngmmgm  48096  rrx2xpref1o  48568  f1omo  48691