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

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 397

This theorem is referenced by:  sylancb  600  rexdifi  4081  reupick3  4254  difprsnss  4733  opthhausdorff  5432  pwssun  5486  trin2  6033  sspred  6215  fundif  6490  fnun  6554  fcoOLD  6634  f1cof1  6690  f1coOLD  6692  f1oun  6744  f1oco  6748  eqfnfv  6918  eqfunfv  6923  sorpsscmpl  7596  ordsucsssuc  7679  ordsucun  7681  soxp  7979  ressuppssdif  8010  frrlem4  8114  wfrlem4OLD  8152  issmo  8188  tfrlem5  8220  ener  8796  domtr  8802  unen  8845  xpdom2  8863  mapen  8937  unxpdomlem3  9038  fiin  9190  suc11reg  9386  djuunxp  9688  xpnum  9718  pm54.43  9768  r0weon  9777  fseqen  9792  kmlem9  9923  axpre-lttrn  10931  axpre-mulgt0  10933  wloglei  11516  mulnzcnopr  11630  zaddcl  12369  zmulcl  12378  qaddcl  12714  qmulcl  12716  rpaddcl  12761  rpmulcl  12762  rpdivcl  12764  xrltnsym  12880  xrlttri  12882  xmullem  13007  xmulcom  13009  xmulneg1  13012  xmulf  13015  ge0addcl  13201  ge0mulcl  13202  ge0xaddcl  13203  ge0xmulcl  13204  serge0  13786  expclzlem  13815  expge0  13828  expge1  13829  hashfacen  14175  hashfacenOLD  14176  wwlktovf1  14681  qredeu  16372  nn0gcdsq  16465  mul4sq  16664  fpwipodrs  18267  pwmnd  18585  gimco  18893  gictr  18900  symgextf1  19038  efgrelexlemb  19365  xrs1mnd  20645  lmimco  21060  lmictra  21061  cctop  22165  iscn2  22398  iscnp2  22399  paste  22454  txuni  22752  txcn  22786  txcmpb  22804  tx2ndc  22811  hmphtr  22943  snfil  23024  supfil  23055  filssufilg  23071  tsmsxp  23315  dscmet  23737  rlimcnp  26124  efnnfsumcl  26261  efchtdvds  26317  lgsne0  26492  mul2sq  26576  colinearalglem2  27284  nb3grprlem2  27757  cplgr3v  27811  crctcshwlkn0  28195  wwlksnextinj  28273  hsn0elch  29619  shscli  29688  hsupss  29712  5oalem6  30030  mdsldmd1i  30702  superpos  30725  bnj110  32847  msubco  33502  poseq  33811  sltsolem1  33887  fnsingle  34230  funimage  34239  funpartfun  34254  bj-nnfan  34939  bj-nnfor  34941  bj-snsetex  35162  bj-snmoore  35293  difunieq  35554  riscer  36155  divrngidl  36195  nn0rppwr  40340  nn0expgcd  40342  dvdsexpnn0  40348  mzpincl  40563  kelac2lem  40896  cllem0  41180  unhe1  41400  tz6.12-1-afv  44677  tz6.12-1-afv2  44744  sprsymrelf1  44959  prmdvdsfmtnof1lem2  45048  uspgrsprf1  45320  2zrngamgm  45508  2zrngmmgm  45515  rrx2xpref1o  46075  f1omo  46199