Theorem syl2anb 604

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  sylancb  606  rexdifi  4087  reupick3  4265  difprsnss  4739  opthhausdorff  5465  pwssun  5517  trin2  6080  sspred  6268  fundif  6541  fnun  6606  f1cof1  6740  f1oun  6793  f1oco  6797  eqfnfv  6978  eqfunfv  6984  sorpsscmpl  7684  ordsucsssuc  7770  ordsucun  7772  resf1extb  7881  soxp  8076  poseq  8105  ressuppssdif  8132  frrlem4  8236  issmo  8285  tfrlem5  8316  ener  8945  domtr  8951  unen  8989  xpdom2  9007  mapen  9076  unxpdomlem3  9165  fiin  9332  suc11reg  9538  djuunxp  9843  xpnum  9873  pm54.43  9923  r0weon  9932  fseqen  9947  kmlem9  10079  axpre-lttrn  11087  axpre-mulgt0  11089  wloglei  11680  mulnzcnf  11794  zaddcl  12565  zmulcl  12574  qaddcl  12913  qmulcl  12915  rpaddcl  12964  rpmulcl  12965  rpdivcl  12967  xrltnsym  13086  xrlttri  13088  xmullem  13214  xmulcom  13216  xmulneg1  13219  xmulf  13222  ge0addcl  13411  ge0mulcl  13412  ge0xaddcl  13413  ge0xmulcl  13414  serge0  14016  expclzlem  14043  expge0  14058  expge1  14059  hashfacen  14414  wwlktovf1  14917  nn0rppwr  16528  nn0expgcd  16531  qredeu  16625  nn0gcdsq  16720  mul4sq  16923  fpwipodrs  18504  pwmnd  18906  gimco  19241  gictr  19249  symgextf1  19394  efgrelexlemb  19723  xrs1mnd  21422  pzriprnglem5  21467  pzriprnglem8  21470  lmimco  21826  lmictra  21827  cctop  22996  iscn2  23228  iscnp2  23229  paste  23284  txuni  23582  txcn  23616  txcmpb  23634  tx2ndc  23641  hmphtr  23773  snfil  23854  supfil  23885  filssufilg  23901  tsmsxp  24145  dscmet  24562  rlimcnp  26954  efnnfsumcl  27091  efchtdvds  27147  lgsne0  27323  mul2sq  27407  ltssolem1  27664  z12addscl  28494  colinearalglem2  29001  nb3grprlem2  29475  cplgr3v  29529  crctcshwlkn0  29914  wwlksnextinj  29992  hsn0elch  31344  shscli  31413  hsupss  31437  5oalem6  31755  mdsldmd1i  32427  superpos  32450  bnj110  35047  msubco  35766  fnsingle  36152  funimage  36161  funpartfun  36178  mpomulnzcnf  36534  bj-nnfan  37104  bj-nnfor  37106  bj-snsetex  37323  bj-axseprep  37434  bj-snmoore  37478  difunieq  37743  riscer  38362  divrngidl  38402  dvdsexpnn0  42818  zaddcom  42961  zmulcom  42965  rimco  43012  rictr  43013  mzpincl  43190  kelac2lem  43516  omcl3g  43786  cllem0  44017  unhe1  44236  permaxun  45462  tz6.12-1-afv  47644  tz6.12-1-afv2  47711  sprsymrelf1  47978  prmdvdsfmtnof1lem2  48070  grictr  48421  usgrexmpl2trifr  48535  gpgprismgr4cycllem7  48599  uspgrsprf1  48645  2zrngamgm  48743  2zrngmmgm  48750  rrx2xpref1o  49216  f1omoOLD  49391