Theorem syl2anb 291

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylancb  418  stdcndc  853  reupick3  3508  difprsnss  3834  trin2  5156  fundif  5402  imadiflem  5437  fnun  5466  fco  5529  f1co  5587  foco  5603  f1oun  5636  f1oco  5639  eqfunfv  5782  ftpg  5870  issmo  6521  tfrlem5  6547  ener  7021  domtr  7027  unen  7060  xpdom2  7084  mapen  7101  pm54.43  7489  axpre-lttrn  8204  axpre-mulgt0  8207  zmulcl  9636  qaddcl  9973  qmulcl  9975  rpaddcl  10016  rpmulcl  10017  rpdivcl  10018  xrltnsym  10132  xrlttri3  10136  ge0addcl  10320  ge0mulcl  10321  ge0xaddcl  10322  expclzaplem  10932  expge0  10944  expge1  10945  hashfacen  11216  qredeu  12802  nn0gcdsq  12905  mul4sq  13100  ballotfilem2  13153  cnovex  15110  iscn2  15114  txuni  15177  txcn  15189  lgsne0  15960  mul2sq  16038