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  4091  reupick3  4271  difprsnss  4743  opthhausdorff  5465  pwssun  5516  trin2  6080  sspred  6268  fundif  6541  fnun  6606  f1cof1  6740  f1oun  6793  f1oco  6797  eqfnfv  6977  eqfunfv  6982  sorpsscmpl  7681  ordsucsssuc  7767  ordsucun  7769  resf1extb  7878  soxp  8072  poseq  8101  ressuppssdif  8128  frrlem4  8232  issmo  8281  tfrlem5  8312  ener  8941  domtr  8947  unen  8985  xpdom2  9003  mapen  9072  unxpdomlem3  9161  fiin  9328  suc11reg  9531  djuunxp  9836  xpnum  9866  pm54.43  9916  r0weon  9925  fseqen  9940  kmlem9  10072  axpre-lttrn  11080  axpre-mulgt0  11082  wloglei  11673  mulnzcnf  11787  zaddcl  12558  zmulcl  12567  qaddcl  12906  qmulcl  12908  rpaddcl  12957  rpmulcl  12958  rpdivcl  12960  xrltnsym  13079  xrlttri  13081  xmullem  13207  xmulcom  13209  xmulneg1  13212  xmulf  13215  ge0addcl  13404  ge0mulcl  13405  ge0xaddcl  13406  ge0xmulcl  13407  serge0  14009  expclzlem  14036  expge0  14051  expge1  14052  hashfacen  14407  wwlktovf1  14910  nn0rppwr  16521  nn0expgcd  16524  qredeu  16618  nn0gcdsq  16713  mul4sq  16916  fpwipodrs  18497  pwmnd  18899  gimco  19234  gictr  19242  symgextf1  19387  efgrelexlemb  19716  xrs1mnd  21430  pzriprnglem5  21475  pzriprnglem8  21478  lmimco  21834  lmictra  21835  cctop  22981  iscn2  23213  iscnp2  23214  paste  23269  txuni  23567  txcn  23601  txcmpb  23619  tx2ndc  23626  hmphtr  23758  snfil  23839  supfil  23870  filssufilg  23886  tsmsxp  24130  dscmet  24547  rlimcnp  26942  efnnfsumcl  27080  efchtdvds  27136  lgsne0  27312  mul2sq  27396  ltssolem1  27653  z12addscl  28483  colinearalglem2  28990  nb3grprlem2  29464  cplgr3v  29518  crctcshwlkn0  29904  wwlksnextinj  29982  hsn0elch  31334  shscli  31403  hsupss  31427  5oalem6  31745  mdsldmd1i  32417  superpos  32440  bnj110  35016  msubco  35729  fnsingle  36115  funimage  36124  funpartfun  36141  mpomulnzcnf  36497  bj-nnfan  37067  bj-nnfor  37069  bj-snsetex  37286  bj-axseprep  37397  bj-snmoore  37441  difunieq  37704  riscer  38323  divrngidl  38363  dvdsexpnn0  42780  zaddcom  42923  zmulcom  42927  rimco  42977  rictr  42979  mzpincl  43180  kelac2lem  43510  omcl3g  43780  cllem0  44011  unhe1  44230  permaxun  45456  tz6.12-1-afv  47634  tz6.12-1-afv2  47701  sprsymrelf1  47968  prmdvdsfmtnof1lem2  48060  grictr  48411  usgrexmpl2trifr  48525  gpgprismgr4cycllem7  48589  uspgrsprf1  48635  2zrngamgm  48733  2zrngmmgm  48740  rrx2xpref1o  49206  f1omoOLD  49381