Theorem syl2anb 598

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 581	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	sylan2b 594	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  600  rexdifi  4102  reupick3  4282  difprsnss  4755  opthhausdorff  5465  pwssun  5516  trin2  6080  sspred  6268  fundif  6541  fnun  6606  f1cof1  6740  f1oun  6793  f1oco  6797  eqfnfv  6976  eqfunfv  6981  sorpsscmpl  7679  ordsucsssuc  7765  ordsucun  7767  resf1extb  7876  soxp  8071  poseq  8100  ressuppssdif  8127  frrlem4  8231  issmo  8280  tfrlem5  8311  ener  8938  domtr  8944  unen  8982  xpdom2  9000  mapen  9069  unxpdomlem3  9158  fiin  9325  suc11reg  9528  djuunxp  9833  xpnum  9863  pm54.43  9913  r0weon  9922  fseqen  9937  kmlem9  10069  axpre-lttrn  11077  axpre-mulgt0  11079  wloglei  11669  mulnzcnf  11783  zaddcl  12531  zmulcl  12540  qaddcl  12878  qmulcl  12880  rpaddcl  12929  rpmulcl  12930  rpdivcl  12932  xrltnsym  13051  xrlttri  13053  xmullem  13179  xmulcom  13181  xmulneg1  13184  xmulf  13187  ge0addcl  13376  ge0mulcl  13377  ge0xaddcl  13378  ge0xmulcl  13379  serge0  13979  expclzlem  14006  expge0  14021  expge1  14022  hashfacen  14377  wwlktovf1  14880  nn0rppwr  16488  nn0expgcd  16491  qredeu  16585  nn0gcdsq  16679  mul4sq  16882  fpwipodrs  18463  pwmnd  18862  gimco  19197  gictr  19205  symgextf1  19350  efgrelexlemb  19679  xrs1mnd  21395  pzriprnglem5  21440  pzriprnglem8  21443  lmimco  21799  lmictra  21800  cctop  22950  iscn2  23182  iscnp2  23183  paste  23238  txuni  23536  txcn  23570  txcmpb  23588  tx2ndc  23595  hmphtr  23727  snfil  23808  supfil  23839  filssufilg  23855  tsmsxp  24099  dscmet  24516  rlimcnp  26931  efnnfsumcl  27069  efchtdvds  27125  lgsne0  27302  mul2sq  27386  ltssolem1  27643  z12addscl  28473  colinearalglem2  28980  nb3grprlem2  29454  cplgr3v  29508  crctcshwlkn0  29894  wwlksnextinj  29972  hsn0elch  31323  shscli  31392  hsupss  31416  5oalem6  31734  mdsldmd1i  32406  superpos  32429  bnj110  35014  msubco  35725  fnsingle  36111  funimage  36120  funpartfun  36137  mpomulnzcnf  36493  bj-nnfan  36949  bj-nnfor  36951  bj-snsetex  37164  bj-snmoore  37314  difunieq  37575  riscer  38185  divrngidl  38225  dvdsexpnn0  42585  zaddcom  42715  zmulcom  42719  rimco  42769  rictr  42771  mzpincl  42972  kelac2lem  43302  omcl3g  43572  cllem0  43803  unhe1  44022  permaxun  45248  tz6.12-1-afv  47416  tz6.12-1-afv2  47483  sprsymrelf1  47738  prmdvdsfmtnof1lem2  47827  grictr  48165  usgrexmpl2trifr  48279  gpgprismgr4cycllem7  48343  uspgrsprf1  48389  2zrngamgm  48487  2zrngmmgm  48494  rrx2xpref1o  48960  f1omoOLD  49135