Theorem syl2anb 597

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 580	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	sylan2b 593	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  599  rexdifi  4173  reupick3  4349  difprsnss  4824  opthhausdorff  5536  pwssun  5590  trin2  6155  sspred  6341  fundif  6627  fnun  6693  fcoOLD  6772  f1cof1  6827  f1coOLD  6829  f1oun  6881  f1oco  6885  eqfnfv  7064  eqfunfv  7069  sorpsscmpl  7769  ordsucsssuc  7859  ordsucun  7861  soxp  8170  poseq  8199  ressuppssdif  8226  frrlem4  8330  wfrlem4OLD  8368  issmo  8404  tfrlem5  8436  ener  9061  domtr  9067  unen  9112  xpdom2  9133  mapen  9207  unxpdomlem3  9315  fiin  9491  suc11reg  9688  djuunxp  9990  xpnum  10020  pm54.43  10070  r0weon  10081  fseqen  10096  kmlem9  10228  axpre-lttrn  11235  axpre-mulgt0  11237  wloglei  11822  mulnzcnf  11936  zaddcl  12683  zmulcl  12692  qaddcl  13030  qmulcl  13032  rpaddcl  13079  rpmulcl  13080  rpdivcl  13082  xrltnsym  13199  xrlttri  13201  xmullem  13326  xmulcom  13328  xmulneg1  13331  xmulf  13334  ge0addcl  13520  ge0mulcl  13521  ge0xaddcl  13522  ge0xmulcl  13523  serge0  14107  expclzlem  14134  expge0  14149  expge1  14150  hashfacen  14503  wwlktovf1  15006  nn0rppwr  16608  nn0expgcd  16611  qredeu  16705  nn0gcdsq  16799  mul4sq  17001  fpwipodrs  18610  pwmnd  18972  gimco  19308  gictr  19316  symgextf1  19463  efgrelexlemb  19792  xrs1mnd  21445  pzriprnglem5  21519  pzriprnglem8  21522  lmimco  21887  lmictra  21888  cctop  23034  iscn2  23267  iscnp2  23268  paste  23323  txuni  23621  txcn  23655  txcmpb  23673  tx2ndc  23680  hmphtr  23812  snfil  23893  supfil  23924  filssufilg  23940  tsmsxp  24184  dscmet  24606  rlimcnp  27026  efnnfsumcl  27164  efchtdvds  27220  lgsne0  27397  mul2sq  27481  sltsolem1  27738  ssltsn  27855  nohalf  28425  colinearalglem2  28940  nb3grprlem2  29416  cplgr3v  29470  crctcshwlkn0  29854  wwlksnextinj  29932  hsn0elch  31280  shscli  31349  hsupss  31373  5oalem6  31691  mdsldmd1i  32363  superpos  32386  bnj110  34834  msubco  35499  fnsingle  35883  funimage  35892  funpartfun  35907  mpomulnzcnf  36265  bj-nnfan  36714  bj-nnfor  36716  bj-snsetex  36929  bj-snmoore  37079  difunieq  37340  riscer  37948  divrngidl  37988  dvdsexpnn0  42321  zaddcom  42428  zmulcom  42432  rimco  42473  rictr  42475  mzpincl  42690  kelac2lem  43021  omcl3g  43296  cllem0  43528  unhe1  43747  tz6.12-1-afv  47089  tz6.12-1-afv2  47156  sprsymrelf1  47370  prmdvdsfmtnof1lem2  47459  grictr  47776  usgrexmpl2trifr  47852  uspgrsprf1  47870  2zrngamgm  47968  2zrngmmgm  47975  rrx2xpref1o  48452  f1omo  48574