Theorem syl2anb 607

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  sylancb  609  rexdifi  4103  reupick3  4282  difprsnss  4758  opthhausdorff  5485  pwssun  5537  trin2  6107  sspred  6293  fundif  6566  fnun  6631  f1cof1  6768  f1oun  6822  f1oco  6826  eqfnfv  7007  eqfunfv  7013  sorpsscmpl  7713  ordsucsssuc  7799  ordsucun  7801  resf1extb  7911  soxp  8104  poseq  8133  ressuppssdif  8160  frrlem4  8265  issmo  8314  tfrlem5  8345  ener  8978  domtr  8984  unen  9022  xpdom2  9040  mapen  9109  unxpdomlem3  9198  fiin  9365  suc11reg  9571  djuunxp  9876  xpnum  9906  pm54.43  9956  r0weon  9965  fseqen  9980  kmlem9  10112  axpre-lttrn  11121  axpre-mulgt0  11123  wloglei  11716  mulnzcnf  11830  zaddcl  12608  zmulcl  12617  qaddcl  12963  qmulcl  12965  rpaddcl  13014  rpmulcl  13015  rpdivcl  13017  xrltnsym  13136  xrlttri  13138  xmullem  13264  xmulcom  13266  xmulneg1  13269  xmulf  13272  ge0addcl  13461  ge0mulcl  13462  ge0xaddcl  13463  ge0xmulcl  13464  serge0  14066  expclzlem  14093  expge0  14108  expge1  14109  hashfacen  14464  wwlktovf1  14967  nn0rppwr  16578  nn0expgcd  16581  qredeu  16675  nn0gcdsq  16770  mul4sq  16973  fpwipodrs  18555  pwmnd  18957  gimco  19291  gictr  19299  symgextf1  19444  efgrelexlemb  19773  xrs1mnd  21472  pzriprnglem5  21517  pzriprnglem8  21520  lmimco  21876  lmictra  21877  cctop  23046  iscn2  23278  iscnp2  23279  paste  23334  txuni  23632  txcn  23666  txcmpb  23684  tx2ndc  23691  hmphtr  23823  snfil  23904  supfil  23935  filssufilg  23951  tsmsxp  24195  dscmet  24612  rlimcnp  27007  efnnfsumcl  27144  efchtdvds  27200  lgsne0  27376  mul2sq  27460  ltssolem1  27716  z12addscl  28547  colinearalglem2  29054  nb3grprlem2  29528  cplgr3v  29582  crctcshwlkn0  29967  wwlksnextinj  30045  hsn0elch  31397  shscli  31466  hsupss  31490  5oalem6  31808  mdsldmd1i  32480  superpos  32503  bnj110  35117  msubco  35845  fnsingle  36231  funimage  36240  funpartfun  36257  mpomulnzcnf  36623  bj-nnfan  37193  bj-nnfor  37195  bj-snsetex  37412  bj-axseprep  37523  bj-snmoore  37567  difunieq  37832  riscer  38451  divrngidl  38491  dvdsexpnn0  42907  zaddcom  43050  zmulcom  43054  rimco  43101  rictr  43102  mzpincl  43279  kelac2lem  43605  omcl3g  43875  cllem0  44106  unhe1  44325  permaxun  45551  tz6.12-1-afv  47732  tz6.12-1-afv2  47799  sprsymrelf1  48066  prmdvdsfmtnof1lem2  48158  grictr  48509  usgrexmpl2trifr  48623  gpgprismgr4cycllem7  48687  uspgrsprf1  48733  2zrngamgm  48831  2zrngmmgm  48838  rrx2xpref1o  49304  f1omoOLD  49479