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

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

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 399

This theorem is referenced by:  sylancb  601  rexdifi  4122  reupick3  4288  difprsnss  4732  opthhausdorff  5407  pwssun  5456  trin2  5983  sspred  6156  fundif  6403  fnun  6463  fco  6531  f1co  6585  foco  6602  f1oun  6634  f1oco  6637  eqfnfv  6802  eqfunfv  6807  sorpsscmpl  7460  ordsucsssuc  7538  ordsucun  7540  soxp  7823  ressuppssdif  7851  wfrlem4  7958  issmo  7985  tfrlem5  8016  ener  8556  domtr  8562  unen  8596  xpdom2  8612  mapen  8681  unxpdomlem3  8724  fiin  8886  suc11reg  9082  djuunxp  9350  xpnum  9380  pm54.43  9429  r0weon  9438  fseqen  9453  kmlem9  9584  axpre-lttrn  10588  axpre-mulgt0  10590  wloglei  11172  mulnzcnopr  11286  zaddcl  12023  zmulcl  12032  qaddcl  12365  qmulcl  12367  rpaddcl  12412  rpmulcl  12413  rpdivcl  12415  xrltnsym  12531  xrlttri  12533  xmullem  12658  xmulcom  12660  xmulneg1  12663  xmulf  12666  ge0addcl  12849  ge0mulcl  12850  ge0xaddcl  12851  ge0xmulcl  12852  serge0  13425  expclzlem  13454  expge0  13466  expge1  13467  hashfacen  13813  wwlktovf1  14321  qredeu  16002  nn0gcdsq  16092  mul4sq  16290  fpwipodrs  17774  pwmnd  18102  gimco  18408  gictr  18415  symgextf1  18549  efgrelexlemb  18876  xrs1mnd  20583  lmimco  20988  lmictra  20989  cctop  21614  iscn2  21846  iscnp2  21847  paste  21902  txuni  22200  txcn  22234  txcmpb  22252  tx2ndc  22259  hmphtr  22391  snfil  22472  supfil  22503  filssufilg  22519  tsmsxp  22763  dscmet  23182  rlimcnp  25543  efnnfsumcl  25680  efchtdvds  25736  lgsne0  25911  mul2sq  25995  colinearalglem2  26693  nb3grprlem2  27163  cplgr3v  27217  crctcshwlkn0  27599  wwlksnextinj  27677  hsn0elch  29025  shscli  29094  hsupss  29118  5oalem6  29436  mdsldmd1i  30108  superpos  30131  bnj110  32130  msubco  32778  poseq  33095  frrlem4  33126  sltsolem1  33180  fnsingle  33380  funimage  33389  funpartfun  33404  bj-nnfan  34077  bj-nnfor  34079  bj-snsetex  34278  bj-snmoore  34408  difunieq  34658  riscer  35281  divrngidl  35321  nn0rppwr  39202  nn0expgcd  39204  mzpincl  39351  kelac2lem  39684  cllem0  39945  unhe1  40151  tz6.12-1-afv  43393  tz6.12-1-afv2  43460  sprsymrelf1  43678  prmdvdsfmtnof1lem2  43767  uspgrsprf1  44042  2zrngamgm  44230  2zrngmmgm  44237  rrx2xpref1o  44725