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  4107  reupick3  4286  difprsnss  4772  opthhausdorff  5505  pwssun  5558  trin2  6128  sspred  6318  fundif  6592  fnun  6656  f1cof1  6793  f1oun  6847  f1oco  6851  eqfnfv  7032  eqfunfv  7038  sorpsscmpl  7744  ordsucsssuc  7828  ordsucun  7830  resf1extb  7940  soxp  8134  poseq  8163  ressuppssdif  8190  frrlem4  8295  issmo  8344  tfrlem5  8375  ener  9007  domtr  9013  unen  9052  xpdom2  9070  mapen  9139  unxpdomlem3  9228  fiin  9392  suc11reg  9598  djuunxp  9926  xpnum  9956  pm54.43  10006  r0weon  10015  fseqen  10030  kmlem9  10161  axpre-lttrn  11169  axpre-mulgt0  11171  wloglei  11764  mulnzcnf  11878  zaddcl  12652  zmulcl  12661  qaddcl  13007  qmulcl  13009  rpaddcl  13058  rpmulcl  13059  rpdivcl  13061  xrltnsym  13180  xrlttri  13182  xmullem  13308  xmulcom  13310  xmulneg1  13313  xmulf  13316  ge0addcl  13505  ge0mulcl  13506  ge0xaddcl  13507  ge0xmulcl  13508  serge0  14112  expclzlem  14139  expge0  14154  expge1  14155  hashfacen  14511  wwlktovf1  15020  nn0rppwr  16644  nn0expgcd  16647  qredeu  16741  nn0gcdsq  16836  mul4sq  17039  fpwipodrs  18621  pwmnd  19030  gimco  19369  gictr  19377  symgextf1  19522  efgrelexlemb  19851  rimco  20632  rictr  20637  xrs1mnd  21627  pzriprnglem5  21672  pzriprnglem8  21675  lmimco  22031  lmictra  22032  cctop  23200  iscn2  23432  iscnp2  23433  paste  23488  txuni  23786  txcn  23820  txcmpb  23838  tx2ndc  23845  hmphtr  23977  snfil  24058  supfil  24089  filssufilg  24105  tsmsxp  24349  dscmet  24766  rlimcnp  27167  efnnfsumcl  27304  efchtdvds  27360  lgsne0  27536  mul2sq  27620  ltssolem1  27876  z12addscl  28707  colinearalglem2  29294  nb3grprlem2  29768  cplgr3v  29822  crctcshwlkn0  30207  wwlksnextinj  30285  hsn0elch  31637  shscli  31706  hsupss  31730  5oalem6  32048  mdsldmd1i  32720  superpos  32743  bnj110  35278  scottsn  35544  msubco  36044  fnsingle  36430  funimage  36439  funpartfun  36456  mpomulnzcnf  36852  bj-nnfan  37420  bj-nnfor  37422  bj-snsetex  37640  bj-axseprep  37752  bj-snmoore  37796  difunieq  38061  riscer  38680  divrngidl  38720  dvdsexpnn0  43136  zaddcom  43279  zmulcom  43283  mzpincl  43506  kelac2lem  43832  omcl3g  44102  cllem0  44333  unhe1  44552  permaxun  45761  tz6.12-1-afv  47952  tz6.12-1-afv2  48019  sprsymrelf1  48286  prmdvdsfmtnof1lem2  48378  grictr  48729  usgrexmpl2trifr  48843  gpgprismgr4cycllem7  48907  uspgrsprf1  48953  2zrngamgm  49051  2zrngmmgm  49058  rrx2xpref1o  49539  f1omoOLD  49713