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  4106  reupick3  4285  difprsnss  4762  opthhausdorff  5491  pwssun  5544  trin2  6114  sspred  6301  fundif  6574  fnun  6639  f1cof1  6776  f1oun  6830  f1oco  6834  eqfnfv  7015  eqfunfv  7021  sorpsscmpl  7721  ordsucsssuc  7807  ordsucun  7809  resf1extb  7919  soxp  8113  poseq  8142  ressuppssdif  8169  frrlem4  8274  issmo  8323  tfrlem5  8354  ener  8986  domtr  8992  unen  9030  xpdom2  9048  mapen  9117  unxpdomlem3  9206  fiin  9370  suc11reg  9576  djuunxp  9895  xpnum  9925  pm54.43  9975  r0weon  9984  fseqen  9999  kmlem9  10130  axpre-lttrn  11139  axpre-mulgt0  11141  wloglei  11734  mulnzcnf  11848  zaddcl  12625  zmulcl  12634  qaddcl  12980  qmulcl  12982  rpaddcl  13031  rpmulcl  13032  rpdivcl  13034  xrltnsym  13153  xrlttri  13155  xmullem  13281  xmulcom  13283  xmulneg1  13286  xmulf  13289  ge0addcl  13478  ge0mulcl  13479  ge0xaddcl  13480  ge0xmulcl  13481  serge0  14083  expclzlem  14110  expge0  14125  expge1  14126  hashfacen  14481  wwlktovf1  14984  nn0rppwr  16609  nn0expgcd  16612  qredeu  16706  nn0gcdsq  16801  mul4sq  17004  fpwipodrs  18586  pwmnd  18989  gimco  19329  gictr  19337  symgextf1  19482  efgrelexlemb  19811  xrs1mnd  21550  pzriprnglem5  21595  pzriprnglem8  21598  lmimco  21954  lmictra  21955  cctop  23124  iscn2  23356  iscnp2  23357  paste  23412  txuni  23710  txcn  23744  txcmpb  23762  tx2ndc  23769  hmphtr  23901  snfil  23982  supfil  24013  filssufilg  24029  tsmsxp  24273  dscmet  24690  rlimcnp  27088  efnnfsumcl  27225  efchtdvds  27281  lgsne0  27457  mul2sq  27541  ltssolem1  27797  z12addscl  28628  colinearalglem2  29166  nb3grprlem2  29640  cplgr3v  29694  crctcshwlkn0  30079  wwlksnextinj  30157  hsn0elch  31509  shscli  31578  hsupss  31602  5oalem6  31920  mdsldmd1i  32592  superpos  32615  bnj110  35163  msubco  35894  fnsingle  36280  funimage  36289  funpartfun  36306  mpomulnzcnf  36672  bj-nnfan  37241  bj-nnfor  37243  bj-snsetex  37460  bj-axseprep  37571  bj-snmoore  37615  difunieq  37880  riscer  38499  divrngidl  38539  dvdsexpnn0  42955  zaddcom  43098  zmulcom  43102  rimco  43149  rictr  43150  mzpincl  43327  kelac2lem  43653  omcl3g  43923  cllem0  44154  unhe1  44373  permaxun  45585  tz6.12-1-afv  47766  tz6.12-1-afv2  47833  sprsymrelf1  48100  prmdvdsfmtnof1lem2  48192  grictr  48543  usgrexmpl2trifr  48657  gpgprismgr4cycllem7  48721  uspgrsprf1  48767  2zrngamgm  48865  2zrngmmgm  48872  rrx2xpref1o  49349  f1omoOLD  49523