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 205   ∧ 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 206  df-an 396

This theorem is referenced by:  sylancb  599  rexdifi  4076  reupick3  4250  difprsnss  4729  opthhausdorff  5425  pwssun  5476  trin2  6017  sspred  6200  fundif  6467  fnun  6529  fcoOLD  6609  f1cof1  6665  f1coOLD  6667  f1oun  6719  f1oco  6722  eqfnfv  6891  eqfunfv  6896  sorpsscmpl  7565  ordsucsssuc  7645  ordsucun  7647  soxp  7941  ressuppssdif  7972  frrlem4  8076  wfrlem4OLD  8114  issmo  8150  tfrlem5  8182  ener  8742  domtr  8748  unen  8790  xpdom2  8807  mapen  8877  unxpdomlem3  8958  fiin  9111  suc11reg  9307  djuunxp  9610  xpnum  9640  pm54.43  9690  r0weon  9699  fseqen  9714  kmlem9  9845  axpre-lttrn  10853  axpre-mulgt0  10855  wloglei  11437  mulnzcnopr  11551  zaddcl  12290  zmulcl  12299  qaddcl  12634  qmulcl  12636  rpaddcl  12681  rpmulcl  12682  rpdivcl  12684  xrltnsym  12800  xrlttri  12802  xmullem  12927  xmulcom  12929  xmulneg1  12932  xmulf  12935  ge0addcl  13121  ge0mulcl  13122  ge0xaddcl  13123  ge0xmulcl  13124  serge0  13705  expclzlem  13734  expge0  13747  expge1  13748  hashfacen  14094  hashfacenOLD  14095  wwlktovf1  14600  qredeu  16291  nn0gcdsq  16384  mul4sq  16583  fpwipodrs  18173  pwmnd  18491  gimco  18799  gictr  18806  symgextf1  18944  efgrelexlemb  19271  xrs1mnd  20548  lmimco  20961  lmictra  20962  cctop  22064  iscn2  22297  iscnp2  22298  paste  22353  txuni  22651  txcn  22685  txcmpb  22703  tx2ndc  22710  hmphtr  22842  snfil  22923  supfil  22954  filssufilg  22970  tsmsxp  23214  dscmet  23634  rlimcnp  26020  efnnfsumcl  26157  efchtdvds  26213  lgsne0  26388  mul2sq  26472  colinearalglem2  27178  nb3grprlem2  27651  cplgr3v  27705  crctcshwlkn0  28087  wwlksnextinj  28165  hsn0elch  29511  shscli  29580  hsupss  29604  5oalem6  29922  mdsldmd1i  30594  superpos  30617  bnj110  32738  msubco  33393  poseq  33729  sltsolem1  33805  fnsingle  34148  funimage  34157  funpartfun  34172  bj-nnfan  34857  bj-nnfor  34859  bj-snsetex  35080  bj-snmoore  35211  difunieq  35472  riscer  36073  divrngidl  36113  nn0rppwr  40254  nn0expgcd  40256  dvdsexpnn0  40262  mzpincl  40472  kelac2lem  40805  cllem0  41062  unhe1  41282  tz6.12-1-afv  44553  tz6.12-1-afv2  44620  sprsymrelf1  44836  prmdvdsfmtnof1lem2  44925  uspgrsprf1  45197  2zrngamgm  45385  2zrngmmgm  45392  rrx2xpref1o  45952  f1omo  46076