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 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  sylancb  601  rexdifi  4146  reupick3  4320  difprsnss  4803  opthhausdorff  5518  pwssun  5572  trin2  6125  sspred  6310  fundif  6598  fnun  6664  fcoOLD  6743  f1cof1  6799  f1coOLD  6801  f1oun  6853  f1oco  6857  eqfnfv  7033  eqfunfv  7038  sorpsscmpl  7724  ordsucsssuc  7811  ordsucun  7813  soxp  8115  poseq  8144  ressuppssdif  8170  frrlem4  8274  wfrlem4OLD  8312  issmo  8348  tfrlem5  8380  ener  8997  domtr  9003  unen  9046  xpdom2  9067  mapen  9141  unxpdomlem3  9252  fiin  9417  suc11reg  9614  djuunxp  9916  xpnum  9946  pm54.43  9996  r0weon  10007  fseqen  10022  kmlem9  10153  axpre-lttrn  11161  axpre-mulgt0  11163  wloglei  11746  mulnzcnopr  11860  zaddcl  12602  zmulcl  12611  qaddcl  12949  qmulcl  12951  rpaddcl  12996  rpmulcl  12997  rpdivcl  12999  xrltnsym  13116  xrlttri  13118  xmullem  13243  xmulcom  13245  xmulneg1  13248  xmulf  13251  ge0addcl  13437  ge0mulcl  13438  ge0xaddcl  13439  ge0xmulcl  13440  serge0  14022  expclzlem  14049  expge0  14064  expge1  14065  hashfacen  14413  hashfacenOLD  14414  wwlktovf1  14908  qredeu  16595  nn0gcdsq  16688  mul4sq  16887  fpwipodrs  18493  pwmnd  18818  gimco  19142  gictr  19149  symgextf1  19289  efgrelexlemb  19618  xrs1mnd  20983  lmimco  21399  lmictra  21400  cctop  22509  iscn2  22742  iscnp2  22743  paste  22798  txuni  23096  txcn  23130  txcmpb  23148  tx2ndc  23155  hmphtr  23287  snfil  23368  supfil  23399  filssufilg  23415  tsmsxp  23659  dscmet  24081  rlimcnp  26470  efnnfsumcl  26607  efchtdvds  26663  lgsne0  26838  mul2sq  26922  sltsolem1  27178  ssltsn  27294  colinearalglem2  28196  nb3grprlem2  28669  cplgr3v  28723  crctcshwlkn0  29106  wwlksnextinj  29184  hsn0elch  30532  shscli  30601  hsupss  30625  5oalem6  30943  mdsldmd1i  31615  superpos  31638  bnj110  33900  msubco  34553  fnsingle  34922  funimage  34931  funpartfun  34946  bj-nnfan  35674  bj-nnfor  35676  bj-snsetex  35892  bj-snmoore  36042  difunieq  36303  riscer  36904  divrngidl  36944  rimco  41141  rictr  41143  nn0rppwr  41272  nn0expgcd  41274  dvdsexpnn0  41280  zaddcom  41373  zmulcom  41377  mzpincl  41520  kelac2lem  41854  omcl3g  42132  cllem0  42365  unhe1  42584  tz6.12-1-afv  45930  tz6.12-1-afv2  45997  sprsymrelf1  46212  prmdvdsfmtnof1lem2  46301  uspgrsprf1  46573  pzriprnglem5  46857  pzriprnglem8  46860  2zrngamgm  46885  2zrngmmgm  46892  rrx2xpref1o  47452  f1omo  47575