Theorem syl2anb 600

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  sylancb  602  rexdifi  4073  reupick3  4240  difprsnss  4692  opthhausdorff  5372  pwssun  5421  trin2  5950  sspred  6124  fundif  6373  fnun  6434  fco  6505  f1co  6560  foco  6577  f1oun  6609  f1oco  6612  eqfnfv  6779  eqfunfv  6784  sorpsscmpl  7440  ordsucsssuc  7518  ordsucun  7520  soxp  7806  ressuppssdif  7834  wfrlem4  7941  issmo  7968  tfrlem5  7999  ener  8539  domtr  8545  unen  8579  xpdom2  8595  mapen  8665  unxpdomlem3  8708  fiin  8870  suc11reg  9066  djuunxp  9334  xpnum  9364  pm54.43  9414  r0weon  9423  fseqen  9438  kmlem9  9569  axpre-lttrn  10577  axpre-mulgt0  10579  wloglei  11161  mulnzcnopr  11275  zaddcl  12010  zmulcl  12019  qaddcl  12352  qmulcl  12354  rpaddcl  12399  rpmulcl  12400  rpdivcl  12402  xrltnsym  12518  xrlttri  12520  xmullem  12645  xmulcom  12647  xmulneg1  12650  xmulf  12653  ge0addcl  12838  ge0mulcl  12839  ge0xaddcl  12840  ge0xmulcl  12841  serge0  13420  expclzlem  13449  expge0  13461  expge1  13462  hashfacen  13808  wwlktovf1  14312  qredeu  15992  nn0gcdsq  16082  mul4sq  16280  fpwipodrs  17766  pwmnd  18094  gimco  18400  gictr  18407  symgextf1  18541  efgrelexlemb  18868  xrs1mnd  20129  lmimco  20533  lmictra  20534  cctop  21611  iscn2  21843  iscnp2  21844  paste  21899  txuni  22197  txcn  22231  txcmpb  22249  tx2ndc  22256  hmphtr  22388  snfil  22469  supfil  22500  filssufilg  22516  tsmsxp  22760  dscmet  23179  rlimcnp  25551  efnnfsumcl  25688  efchtdvds  25744  lgsne0  25919  mul2sq  26003  colinearalglem2  26701  nb3grprlem2  27171  cplgr3v  27225  crctcshwlkn0  27607  wwlksnextinj  27685  hsn0elch  29031  shscli  29100  hsupss  29124  5oalem6  29442  mdsldmd1i  30114  superpos  30137  bnj110  32240  msubco  32891  poseq  33208  frrlem4  33239  sltsolem1  33293  fnsingle  33493  funimage  33502  funpartfun  33517  bj-nnfan  34192  bj-nnfor  34194  bj-snsetex  34399  bj-snmoore  34528  difunieq  34791  riscer  35426  divrngidl  35466  nn0rppwr  39490  nn0expgcd  39492  mzpincl  39675  kelac2lem  40008  cllem0  40265  unhe1  40486  tz6.12-1-afv  43730  tz6.12-1-afv2  43797  sprsymrelf1  44013  prmdvdsfmtnof1lem2  44102  uspgrsprf1  44375  2zrngamgm  44563  2zrngmmgm  44570  rrx2xpref1o  45132