Theorem syl2anb 596

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 579	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	sylan2b 592	1 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 395

This theorem is referenced by:  sylancb  598  rexdifi  4146  reupick3  4323  difprsnss  4807  opthhausdorff  5523  pwssun  5577  trin2  6134  sspred  6319  fundif  6607  fnun  6673  fcoOLD  6753  f1cof1  6809  f1coOLD  6811  f1oun  6863  f1oco  6867  eqfnfv  7045  eqfunfv  7050  sorpsscmpl  7745  ordsucsssuc  7832  ordsucun  7834  soxp  8140  poseq  8169  ressuppssdif  8196  frrlem4  8301  wfrlem4OLD  8339  issmo  8375  tfrlem5  8407  ener  9028  domtr  9034  unen  9077  xpdom2  9098  mapen  9172  unxpdomlem3  9283  fiin  9453  suc11reg  9650  djuunxp  9952  xpnum  9982  pm54.43  10032  r0weon  10043  fseqen  10058  kmlem9  10189  axpre-lttrn  11197  axpre-mulgt0  11199  wloglei  11784  mulnzcnf  11898  zaddcl  12640  zmulcl  12649  qaddcl  12987  qmulcl  12989  rpaddcl  13036  rpmulcl  13037  rpdivcl  13039  xrltnsym  13156  xrlttri  13158  xmullem  13283  xmulcom  13285  xmulneg1  13288  xmulf  13291  ge0addcl  13477  ge0mulcl  13478  ge0xaddcl  13479  ge0xmulcl  13480  serge0  14061  expclzlem  14088  expge0  14103  expge1  14104  hashfacen  14453  hashfacenOLD  14454  wwlktovf1  14948  qredeu  16636  nn0gcdsq  16731  mul4sq  16930  fpwipodrs  18539  pwmnd  18896  gimco  19229  gictr  19237  symgextf1  19383  efgrelexlemb  19712  xrs1mnd  21344  pzriprnglem5  21418  pzriprnglem8  21421  lmimco  21785  lmictra  21786  cctop  22929  iscn2  23162  iscnp2  23163  paste  23218  txuni  23516  txcn  23550  txcmpb  23568  tx2ndc  23575  hmphtr  23707  snfil  23788  supfil  23819  filssufilg  23835  tsmsxp  24079  dscmet  24501  rlimcnp  26917  efnnfsumcl  27055  efchtdvds  27111  lgsne0  27288  mul2sq  27372  sltsolem1  27628  ssltsn  27745  colinearalglem2  28738  nb3grprlem2  29214  cplgr3v  29268  crctcshwlkn0  29652  wwlksnextinj  29730  hsn0elch  31078  shscli  31147  hsupss  31171  5oalem6  31489  mdsldmd1i  32161  superpos  32184  bnj110  34522  msubco  35174  fnsingle  35548  funimage  35557  funpartfun  35572  mpomulnzcnf  35816  bj-nnfan  36258  bj-nnfor  36260  bj-snsetex  36475  bj-snmoore  36625  difunieq  36886  riscer  37494  divrngidl  37534  rimco  41786  rictr  41788  nn0rppwr  41924  nn0expgcd  41926  dvdsexpnn0  41932  zaddcom  42038  zmulcom  42042  mzpincl  42185  kelac2lem  42519  omcl3g  42794  cllem0  43027  unhe1  43246  tz6.12-1-afv  46583  tz6.12-1-afv2  46650  sprsymrelf1  46865  prmdvdsfmtnof1lem2  46954  grictr  47267  uspgrsprf1  47287  2zrngamgm  47385  2zrngmmgm  47392  rrx2xpref1o  47869  f1omo  47991