Theorem syl2anb 610

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 593	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	sylan2b 606	1 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sylancb  612  rexdifi  4100  reupick3  4279  difprsnss  4765  opthhausdorff  5498  pwssun  5551  trin2  6121  sspred  6312  fundif  6586  fnun  6650  f1cof1  6787  f1oun  6841  f1oco  6845  eqfnfv  7026  eqfunfv  7032  sorpsscmpl  7739  ordsucsssuc  7823  ordsucun  7825  resf1extb  7935  soxp  8131  poseq  8160  ressuppssdif  8187  frrlem4  8292  issmo  8341  tfrlem5  8372  ener  9011  domtr  9017  unen  9056  xpdom2  9074  mapen  9143  unxpdomlem3  9232  fiin  9396  suc11reg  9602  djuunxp  9930  xpnum  9960  pm54.43  10010  r0weon  10019  fseqen  10034  kmlem9  10165  axpre-lttrn  11179  axpre-mulgt0  11181  wloglei  11774  mulnzcnf  11888  zaddcl  12662  zmulcl  12671  qaddcl  13019  qmulcl  13021  rpaddcl  13070  rpmulcl  13071  rpdivcl  13073  xrltnsym  13192  xrlttri  13194  xmullem  13320  xmulcom  13322  xmulneg1  13325  xmulf  13328  ge0addcl  13517  ge0mulcl  13518  ge0xaddcl  13519  ge0xmulcl  13520  serge0  14124  expclzlem  14151  expge0  14166  expge1  14167  hashfacen  14523  wwlktovf1  15034  nn0rppwr  16657  nn0expgcd  16660  qredeu  16754  nn0gcdsq  16849  mul4sq  17052  fpwipodrs  18634  pwmnd  19062  gimco  19401  gictr  19409  symgextf1  19554  efgrelexlemb  19883  rimco  20664  rictr  20669  xrs1mnd  21659  pzriprnglem5  21704  pzriprnglem8  21707  lmimco  22063  lmictra  22064  cctop  23237  iscn2  23469  iscnp2  23470  paste  23525  txuni  23824  txcn  23858  txcmpb  23876  tx2ndc  23883  hmphtr  24015  snfil  24096  supfil  24127  filssufilg  24143  tsmsxp  24387  dscmet  24804  rlimcnp  27210  efnnfsumcl  27347  efchtdvds  27403  lgsne0  27579  mul2sq  27663  ltssolem1  27919  z12addscl  28750  colinearalglem2  29372  nb3grprlem2  29849  cplgr3v  29903  crctcshwlkn0  30297  wwlksnextinj  30375  hsn0elch  31737  shscli  31806  hsupss  31830  5oalem6  32148  mdsldmd1i  32820  superpos  32843  bnj110  35375  scottsn  35641  msubco  36118  fnsingle  36504  funimage  36513  funpartfun  36530  mpomulnzcnf  36927  bj-nnfan  37495  bj-nnfor  37497  bj-snsetex  37715  bj-axseprep  37827  bj-snmoore  37871  difunieq  38136  riscer  38746  divrngidl  38786  dvdsexpnn0  43217  zaddcom  43360  zmulcom  43364  mzpincl  43587  kelac2lem  43913  omcl3g  44183  cllem0  44414  unhe1  44633  permaxun  45842  tz6.12-1-afv  48070  tz6.12-1-afv2  48137  sprsymrelf1  48404  prmdvdsfmtnof1lem2  48496  grictr  48847  usgrexmpl2trifr  48961  gpgprismgr4cycllem7  49025  uspgrsprf1  49071  2zrngamgm  49168  2zrngmmgm  49175  rrx2xpref1o  49656  f1omoOLD  49828