Theorem syl2anb 599

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  sylancb  601  rexdifi  4146  reupick3  4320  difprsnss  4803  opthhausdorff  5518  pwssun  5572  trin2  6125  sspred  6310  fundif  6598  fnun  6664  fcoOLD  6743  f1cof1  6799  f1coOLD  6801  f1oun  6853  f1oco  6857  eqfnfv  7033  eqfunfv  7038  sorpsscmpl  7724  ordsucsssuc  7811  ordsucun  7813  soxp  8115  poseq  8144  ressuppssdif  8170  frrlem4  8274  wfrlem4OLD  8312  issmo  8348  tfrlem5  8380  ener  8997  domtr  9003  unen  9046  xpdom2  9067  mapen  9141  unxpdomlem3  9252  fiin  9417  suc11reg  9614  djuunxp  9916  xpnum  9946  pm54.43  9996  r0weon  10007  fseqen  10022  kmlem9  10153  axpre-lttrn  11161  axpre-mulgt0  11163  wloglei  11746  mulnzcnopr  11860  zaddcl  12602  zmulcl  12611  qaddcl  12949  qmulcl  12951  rpaddcl  12996  rpmulcl  12997  rpdivcl  12999  xrltnsym  13116  xrlttri  13118  xmullem  13243  xmulcom  13245  xmulneg1  13248  xmulf  13251  ge0addcl  13437  ge0mulcl  13438  ge0xaddcl  13439  ge0xmulcl  13440  serge0  14022  expclzlem  14049  expge0  14064  expge1  14065  hashfacen  14413  hashfacenOLD  14414  wwlktovf1  14908  qredeu  16595  nn0gcdsq  16688  mul4sq  16887  fpwipodrs  18493  pwmnd  18818  gimco  19142  gictr  19149  symgextf1  19289  efgrelexlemb  19618  xrs1mnd  20983  lmimco  21399  lmictra  21400  cctop  22509  iscn2  22742  iscnp2  22743  paste  22798  txuni  23096  txcn  23130  txcmpb  23148  tx2ndc  23155  hmphtr  23287  snfil  23368  supfil  23399  filssufilg  23415  tsmsxp  23659  dscmet  24081  rlimcnp  26470  efnnfsumcl  26607  efchtdvds  26663  lgsne0  26838  mul2sq  26922  sltsolem1  27178  colinearalglem2  28165  nb3grprlem2  28638  cplgr3v  28692  crctcshwlkn0  29075  wwlksnextinj  29153  hsn0elch  30501  shscli  30570  hsupss  30594  5oalem6  30912  mdsldmd1i  31584  superpos  31607  bnj110  33869  msubco  34522  fnsingle  34891  funimage  34900  funpartfun  34915  bj-nnfan  35626  bj-nnfor  35628  bj-snsetex  35844  bj-snmoore  35994  difunieq  36255  riscer  36856  divrngidl  36896  rimco  41093  rictr  41095  nn0rppwr  41224  nn0expgcd  41226  dvdsexpnn0  41232  zaddcom  41325  zmulcom  41329  mzpincl  41472  kelac2lem  41806  omcl3g  42084  cllem0  42317  unhe1  42536  tz6.12-1-afv  45882  tz6.12-1-afv2  45949  sprsymrelf1  46164  prmdvdsfmtnof1lem2  46253  uspgrsprf1  46525  pzriprnglem5  46809  pzriprnglem8  46812  2zrngamgm  46837  2zrngmmgm  46844  rrx2xpref1o  47404  f1omo  47527