Theorem syl2anb 610

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sylancb  612  rexdifi  4086  reupick3  4275  difprsnss  4758  opthhausdorff  5489  pwssun  5542  trin2  6116  sspred  6313  fundif  6589  fnun  6653  f1cof1  6790  f1oun  6844  f1oco  6848  eqfnfv  7029  eqfunfv  7035  sorpsscmpl  7750  ordsucsssuc  7834  ordsucun  7836  resf1extb  7946  soxp  8143  poseq  8177  ressuppssdif  8205  frrlem4  8310  issmo  8359  tfrlem5  8390  ener  9031  domtr  9037  unen  9076  xpdom2  9094  mapen  9163  unxpdomlem3  9252  fiin  9417  suc11reg  9623  djuunxp  10005  xpnum  10035  pm54.43  10085  r0weon  10094  fseqen  10109  kmlem9  10240  axpre-lttrn  11254  axpre-mulgt0  11256  wloglei  11851  mulnzcnf  11965  zaddcl  12739  zmulcl  12748  qaddcl  13096  qmulcl  13098  rpaddcl  13147  rpmulcl  13148  rpdivcl  13150  xrltnsym  13269  xrlttri  13271  xmullem  13397  xmulcom  13399  xmulneg1  13402  xmulf  13405  ge0addcl  13594  ge0mulcl  13595  ge0xaddcl  13596  ge0xmulcl  13597  serge0  14202  expclzlem  14229  expge0  14244  expge1  14245  hashfacen  14602  wwlktovf1  15115  nn0rppwr  16740  nn0expgcd  16743  qredeu  16838  nn0gcdsq  16933  mul4sq  17137  fpwipodrs  18719  pwmnd  19148  gimco  19487  gictr  19495  symgextf1  19640  efgrelexlemb  19969  rimco  20752  rictr  20757  xrs1mnd  21751  pzriprnglem5  21796  pzriprnglem8  21799  lmimco  22155  lmictra  22156  cctop  23329  iscn2  23561  iscnp2  23562  paste  23617  txuni  23916  txcn  23950  txcmpb  23968  tx2ndc  23975  hmphtr  24107  snfil  24188  supfil  24219  filssufilg  24235  tsmsxp  24479  dscmet  24896  rlimcnp  27298  efnnfsumcl  27435  efchtdvds  27491  lgsne0  27667  mul2sq  27751  ltssolem1  28037  z12addscl  28868  colinearalglem2  29490  nb3grprlem2  29967  cplgr3v  30021  crctcshwlkn0  30415  wwlksnextinj  30493  hsn0elch  31855  shscli  31924  hsupss  31948  5oalem6  32266  mdsldmd1i  32938  superpos  32961  bnj110  35534  scottsn  35804  msubco  36382  fnsingle  36773  funimage  36782  funpartfun  36799  mpomulnzcnf  37180  bj-nnfan  37748  bj-nnfor  37750  bj-snsetex  37968  bj-axseprep  38082  bj-snmoore  38126  difunieq  38390  riscer  39015  divrngidl  39055  dvdsexpnn0  43479  zaddcom  43621  zmulcom  43625  mzpincl  43838  kelac2lem  44159  omcl3g  44429  cllem0  44660  unhe1  44878  permaxun  46094  tz6.12-1-afv  48337  tz6.12-1-afv2  48404  sprsymrelf1  48671  prmdvdsfmtnof1lem2  48763  grictr  49114  usgrexmpl2trifr  49228  gpgprismgr4cycllem7  49292  uspgrsprf1  49338  2zrngamgm  49435  2zrngmmgm  49442  f1omoOLD  50101