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  4130  reupick3  4310  difprsnss  4780  opthhausdorff  5497  pwssun  5550  trin2  6117  sspred  6304  fundif  6590  fnun  6657  f1cof1  6789  f1oun  6842  f1oco  6846  eqfnfv  7026  eqfunfv  7031  sorpsscmpl  7733  ordsucsssuc  7822  ordsucun  7824  resf1extb  7935  soxp  8133  poseq  8162  ressuppssdif  8189  frrlem4  8293  wfrlem4OLD  8331  issmo  8367  tfrlem5  8399  ener  9020  domtr  9026  unen  9065  xpdom2  9086  mapen  9160  unxpdomlem3  9265  fiin  9439  suc11reg  9638  djuunxp  9940  xpnum  9970  pm54.43  10020  r0weon  10031  fseqen  10046  kmlem9  10178  axpre-lttrn  11185  axpre-mulgt0  11187  wloglei  11774  mulnzcnf  11888  zaddcl  12637  zmulcl  12646  qaddcl  12986  qmulcl  12988  rpaddcl  13036  rpmulcl  13037  rpdivcl  13039  xrltnsym  13158  xrlttri  13160  xmullem  13285  xmulcom  13287  xmulneg1  13290  xmulf  13293  ge0addcl  13482  ge0mulcl  13483  ge0xaddcl  13484  ge0xmulcl  13485  serge0  14079  expclzlem  14106  expge0  14121  expge1  14122  hashfacen  14477  wwlktovf1  14981  nn0rppwr  16585  nn0expgcd  16588  qredeu  16682  nn0gcdsq  16776  mul4sq  16979  fpwipodrs  18555  pwmnd  18920  gimco  19256  gictr  19264  symgextf1  19407  efgrelexlemb  19736  xrs1mnd  21377  pzriprnglem5  21451  pzriprnglem8  21454  lmimco  21809  lmictra  21810  cctop  22949  iscn2  23181  iscnp2  23182  paste  23237  txuni  23535  txcn  23569  txcmpb  23587  tx2ndc  23594  hmphtr  23726  snfil  23807  supfil  23838  filssufilg  23854  tsmsxp  24098  dscmet  24516  rlimcnp  26932  efnnfsumcl  27070  efchtdvds  27126  lgsne0  27303  mul2sq  27387  sltsolem1  27644  ssltsn  27761  colinearalglem2  28891  nb3grprlem2  29365  cplgr3v  29419  crctcshwlkn0  29808  wwlksnextinj  29886  hsn0elch  31234  shscli  31303  hsupss  31327  5oalem6  31645  mdsldmd1i  32317  superpos  32340  bnj110  34894  msubco  35558  fnsingle  35942  funimage  35951  funpartfun  35966  mpomulnzcnf  36322  bj-nnfan  36771  bj-nnfor  36773  bj-snsetex  36986  bj-snmoore  37136  difunieq  37397  riscer  38017  divrngidl  38057  dvdsexpnn0  42352  zaddcom  42470  zmulcom  42474  rimco  42516  rictr  42518  mzpincl  42732  kelac2lem  43063  omcl3g  43333  cllem0  43565  unhe1  43784  permaxun  45011  tz6.12-1-afv  47183  tz6.12-1-afv2  47250  sprsymrelf1  47490  prmdvdsfmtnof1lem2  47579  grictr  47916  usgrexmpl2trifr  48021  gpgprismgr4cycllem7  48080  uspgrsprf1  48102  2zrngamgm  48200  2zrngmmgm  48207  rrx2xpref1o  48678  f1omo  48848