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  4116  reupick3  4296  difprsnss  4766  opthhausdorff  5480  pwssun  5533  trin2  6099  sspred  6286  fundif  6568  fnun  6635  f1cof1  6769  f1oun  6822  f1oco  6826  eqfnfv  7006  eqfunfv  7011  sorpsscmpl  7713  ordsucsssuc  7801  ordsucun  7803  resf1extb  7913  soxp  8111  poseq  8140  ressuppssdif  8167  frrlem4  8271  issmo  8320  tfrlem5  8351  ener  8975  domtr  8981  unen  9020  xpdom2  9041  mapen  9111  unxpdomlem3  9206  fiin  9380  suc11reg  9579  djuunxp  9881  xpnum  9911  pm54.43  9961  r0weon  9972  fseqen  9987  kmlem9  10119  axpre-lttrn  11126  axpre-mulgt0  11128  wloglei  11717  mulnzcnf  11831  zaddcl  12580  zmulcl  12589  qaddcl  12931  qmulcl  12933  rpaddcl  12982  rpmulcl  12983  rpdivcl  12985  xrltnsym  13104  xrlttri  13106  xmullem  13231  xmulcom  13233  xmulneg1  13236  xmulf  13239  ge0addcl  13428  ge0mulcl  13429  ge0xaddcl  13430  ge0xmulcl  13431  serge0  14028  expclzlem  14055  expge0  14070  expge1  14071  hashfacen  14426  wwlktovf1  14930  nn0rppwr  16538  nn0expgcd  16541  qredeu  16635  nn0gcdsq  16729  mul4sq  16932  fpwipodrs  18506  pwmnd  18871  gimco  19207  gictr  19215  symgextf1  19358  efgrelexlemb  19687  xrs1mnd  21328  pzriprnglem5  21402  pzriprnglem8  21405  lmimco  21760  lmictra  21761  cctop  22900  iscn2  23132  iscnp2  23133  paste  23188  txuni  23486  txcn  23520  txcmpb  23538  tx2ndc  23545  hmphtr  23677  snfil  23758  supfil  23789  filssufilg  23805  tsmsxp  24049  dscmet  24467  rlimcnp  26882  efnnfsumcl  27020  efchtdvds  27076  lgsne0  27253  mul2sq  27337  sltsolem1  27594  ssltsn  27711  colinearalglem2  28841  nb3grprlem2  29315  cplgr3v  29369  crctcshwlkn0  29758  wwlksnextinj  29836  hsn0elch  31184  shscli  31253  hsupss  31277  5oalem6  31595  mdsldmd1i  32267  superpos  32290  bnj110  34855  msubco  35525  fnsingle  35914  funimage  35923  funpartfun  35938  mpomulnzcnf  36294  bj-nnfan  36743  bj-nnfor  36745  bj-snsetex  36958  bj-snmoore  37108  difunieq  37369  riscer  37989  divrngidl  38029  dvdsexpnn0  42329  zaddcom  42459  zmulcom  42463  rimco  42513  rictr  42515  mzpincl  42729  kelac2lem  43060  omcl3g  43330  cllem0  43562  unhe1  43781  permaxun  45008  tz6.12-1-afv  47179  tz6.12-1-afv2  47246  sprsymrelf1  47501  prmdvdsfmtnof1lem2  47590  grictr  47927  usgrexmpl2trifr  48032  gpgprismgr4cycllem7  48095  uspgrsprf1  48139  2zrngamgm  48237  2zrngmmgm  48244  rrx2xpref1o  48711  f1omoOLD  48886