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  4100  reupick3  4280  difprsnss  4751  opthhausdorff  5457  pwssun  5508  trin2  6070  sspred  6257  fundif  6530  fnun  6595  f1cof1  6729  f1oun  6782  f1oco  6786  eqfnfv  6964  eqfunfv  6969  sorpsscmpl  7667  ordsucsssuc  7753  ordsucun  7755  resf1extb  7864  soxp  8059  poseq  8088  ressuppssdif  8115  frrlem4  8219  issmo  8268  tfrlem5  8299  ener  8923  domtr  8929  unen  8967  xpdom2  8985  mapen  9054  unxpdomlem3  9142  fiin  9306  suc11reg  9509  djuunxp  9811  xpnum  9841  pm54.43  9891  r0weon  9900  fseqen  9915  kmlem9  10047  axpre-lttrn  11054  axpre-mulgt0  11056  wloglei  11646  mulnzcnf  11760  zaddcl  12509  zmulcl  12518  qaddcl  12860  qmulcl  12862  rpaddcl  12911  rpmulcl  12912  rpdivcl  12914  xrltnsym  13033  xrlttri  13035  xmullem  13160  xmulcom  13162  xmulneg1  13165  xmulf  13168  ge0addcl  13357  ge0mulcl  13358  ge0xaddcl  13359  ge0xmulcl  13360  serge0  13960  expclzlem  13987  expge0  14002  expge1  14003  hashfacen  14358  wwlktovf1  14861  nn0rppwr  16469  nn0expgcd  16472  qredeu  16566  nn0gcdsq  16660  mul4sq  16863  fpwipodrs  18443  pwmnd  18842  gimco  19178  gictr  19186  symgextf1  19331  efgrelexlemb  19660  xrs1mnd  21375  pzriprnglem5  21420  pzriprnglem8  21423  lmimco  21779  lmictra  21780  cctop  22919  iscn2  23151  iscnp2  23152  paste  23207  txuni  23505  txcn  23539  txcmpb  23557  tx2ndc  23564  hmphtr  23696  snfil  23777  supfil  23808  filssufilg  23824  tsmsxp  24068  dscmet  24485  rlimcnp  26900  efnnfsumcl  27038  efchtdvds  27094  lgsne0  27271  mul2sq  27355  sltsolem1  27612  zs12addscl  28385  colinearalglem2  28883  nb3grprlem2  29357  cplgr3v  29411  crctcshwlkn0  29797  wwlksnextinj  29875  hsn0elch  31223  shscli  31292  hsupss  31316  5oalem6  31634  mdsldmd1i  32306  superpos  32329  bnj110  34865  msubco  35563  fnsingle  35952  funimage  35961  funpartfun  35976  mpomulnzcnf  36332  bj-nnfan  36781  bj-nnfor  36783  bj-snsetex  36996  bj-snmoore  37146  difunieq  37407  riscer  38027  divrngidl  38067  dvdsexpnn0  42366  zaddcom  42496  zmulcom  42500  rimco  42550  rictr  42552  mzpincl  42766  kelac2lem  43096  omcl3g  43366  cllem0  43598  unhe1  43817  permaxun  45043  tz6.12-1-afv  47204  tz6.12-1-afv2  47271  sprsymrelf1  47526  prmdvdsfmtnof1lem2  47615  grictr  47953  usgrexmpl2trifr  48067  gpgprismgr4cycllem7  48131  uspgrsprf1  48177  2zrngamgm  48275  2zrngmmgm  48282  rrx2xpref1o  48749  f1omoOLD  48924