Theorem syl2anb 609

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

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

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 401

This theorem is used by:  sylancb  611  rexdifi  4103  reupick3  4282  difprsnss  4766  opthhausdorff  5499  pwssun  5552  trin2  6122  sspred  6311  fundif  6585  fnun  6649  f1cof1  6786  f1oun  6840  f1oco  6844  eqfnfv  7025  eqfunfv  7031  sorpsscmpl  7733  ordsucsssuc  7817  ordsucun  7819  resf1extb  7929  soxp  8123  poseq  8152  ressuppssdif  8179  frrlem4  8284  issmo  8333  tfrlem5  8364  ener  8996  domtr  9002  unen  9040  xpdom2  9058  mapen  9127  unxpdomlem3  9216  fiin  9380  suc11reg  9586  djuunxp  9914  xpnum  9944  pm54.43  9994  r0weon  10003  fseqen  10018  kmlem9  10149  axpre-lttrn  11157  axpre-mulgt0  11159  wloglei  11752  mulnzcnf  11866  zaddcl  12640  zmulcl  12649  qaddcl  12995  qmulcl  12997  rpaddcl  13046  rpmulcl  13047  rpdivcl  13049  xrltnsym  13168  xrlttri  13170  xmullem  13296  xmulcom  13298  xmulneg1  13301  xmulf  13304  ge0addcl  13493  ge0mulcl  13494  ge0xaddcl  13495  ge0xmulcl  13496  serge0  14099  expclzlem  14126  expge0  14141  expge1  14142  hashfacen  14498  wwlktovf1  15001  nn0rppwr  16625  nn0expgcd  16628  qredeu  16722  nn0gcdsq  16817  mul4sq  17020  fpwipodrs  18602  pwmnd  19005  gimco  19344  gictr  19352  symgextf1  19497  efgrelexlemb  19826  rimco  20606  rictr  20611  xrs1mnd  21601  pzriprnglem5  21646  pzriprnglem8  21649  lmimco  22005  lmictra  22006  cctop  23174  iscn2  23406  iscnp2  23407  paste  23462  txuni  23760  txcn  23794  txcmpb  23812  tx2ndc  23819  hmphtr  23951  snfil  24032  supfil  24063  filssufilg  24079  tsmsxp  24323  dscmet  24740  rlimcnp  27141  efnnfsumcl  27278  efchtdvds  27334  lgsne0  27510  mul2sq  27594  ltssolem1  27850  z12addscl  28681  colinearalglem2  29268  nb3grprlem2  29742  cplgr3v  29796  crctcshwlkn0  30181  wwlksnextinj  30259  hsn0elch  31611  shscli  31680  hsupss  31704  5oalem6  32022  mdsldmd1i  32694  superpos  32717  bnj110  35255  scottsn  35528  msubco  36031  fnsingle  36417  funimage  36426  funpartfun  36443  mpomulnzcnf  36839  bj-nnfan  37407  bj-nnfor  37409  bj-snsetex  37627  bj-axseprep  37739  bj-snmoore  37783  difunieq  38048  riscer  38667  divrngidl  38707  dvdsexpnn0  43123  zaddcom  43266  zmulcom  43270  mzpincl  43493  kelac2lem  43819  omcl3g  44089  cllem0  44320  unhe1  44539  permaxun  45748  tz6.12-1-afv  47939  tz6.12-1-afv2  48006  sprsymrelf1  48273  prmdvdsfmtnof1lem2  48365  grictr  48716  usgrexmpl2trifr  48830  gpgprismgr4cycllem7  48894  uspgrsprf1  48940  2zrngamgm  49038  2zrngmmgm  49045  rrx2xpref1o  49526  f1omoOLD  49700