Theorem syl2anb 609

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  sylancb  611  rexdifi  4105  reupick3  4284  difprsnss  4768  opthhausdorff  5502  pwssun  5555  trin2  6125  sspred  6313  fundif  6587  fnun  6651  f1cof1  6788  f1oun  6842  f1oco  6846  eqfnfv  7027  eqfunfv  7033  sorpsscmpl  7733  ordsucsssuc  7820  ordsucun  7822  resf1extb  7932  soxp  8126  poseq  8155  ressuppssdif  8182  frrlem4  8287  issmo  8336  tfrlem5  8367  ener  8999  domtr  9005  unen  9043  xpdom2  9061  mapen  9130  unxpdomlem3  9219  fiin  9383  suc11reg  9589  djuunxp  9908  xpnum  9938  pm54.43  9988  r0weon  9997  fseqen  10012  kmlem9  10143  axpre-lttrn  11152  axpre-mulgt0  11154  wloglei  11747  mulnzcnf  11861  zaddcl  12635  zmulcl  12644  qaddcl  12990  qmulcl  12992  rpaddcl  13041  rpmulcl  13042  rpdivcl  13044  xrltnsym  13163  xrlttri  13165  xmullem  13291  xmulcom  13293  xmulneg1  13296  xmulf  13299  ge0addcl  13488  ge0mulcl  13489  ge0xaddcl  13490  ge0xmulcl  13491  serge0  14094  expclzlem  14121  expge0  14136  expge1  14137  hashfacen  14493  wwlktovf1  14996  nn0rppwr  16620  nn0expgcd  16623  qredeu  16717  nn0gcdsq  16812  mul4sq  17015  fpwipodrs  18597  pwmnd  19000  gimco  19339  gictr  19347  symgextf1  19492  efgrelexlemb  19821  xrs1mnd  21571  pzriprnglem5  21616  pzriprnglem8  21619  lmimco  21975  lmictra  21976  cctop  23144  iscn2  23376  iscnp2  23377  paste  23432  txuni  23730  txcn  23764  txcmpb  23782  tx2ndc  23789  hmphtr  23921  snfil  24002  supfil  24033  filssufilg  24049  tsmsxp  24293  dscmet  24710  rlimcnp  27108  efnnfsumcl  27245  efchtdvds  27301  lgsne0  27477  mul2sq  27561  ltssolem1  27817  z12addscl  28648  colinearalglem2  29235  nb3grprlem2  29709  cplgr3v  29763  crctcshwlkn0  30148  wwlksnextinj  30226  hsn0elch  31578  shscli  31647  hsupss  31671  5oalem6  31989  mdsldmd1i  32661  superpos  32684  bnj110  35224  scottsn  35498  msubco  36001  fnsingle  36387  funimage  36396  funpartfun  36413  mpomulnzcnf  36789  bj-nnfan  37357  bj-nnfor  37359  bj-snsetex  37577  bj-axseprep  37689  bj-snmoore  37733  difunieq  37998  riscer  38617  divrngidl  38657  dvdsexpnn0  43073  zaddcom  43216  zmulcom  43220  rimco  43267  rictr  43268  mzpincl  43445  kelac2lem  43771  omcl3g  44041  cllem0  44272  unhe1  44491  permaxun  45700  tz6.12-1-afv  47888  tz6.12-1-afv2  47955  sprsymrelf1  48222  prmdvdsfmtnof1lem2  48314  grictr  48665  usgrexmpl2trifr  48779  gpgprismgr4cycllem7  48843  uspgrsprf1  48889  2zrngamgm  48987  2zrngmmgm  48994  rrx2xpref1o  49475  f1omoOLD  49649