Theorem syl2anb 289

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylancb  414  stdcndc  830  reupick3  3361  difprsnss  3658  trin2  4930  imadiflem  5202  fnun  5229  fco  5288  f1co  5340  foco  5355  f1oun  5387  f1oco  5390  eqfunfv  5523  ftpg  5604  issmo  6185  tfrlem5  6211  ener  6673  domtr  6679  unen  6710  xpdom2  6725  mapen  6740  pm54.43  7046  axpre-lttrn  7699  axpre-mulgt0  7702  zmulcl  9114  qaddcl  9434  qmulcl  9436  rpaddcl  9472  rpmulcl  9473  rpdivcl  9474  xrltnsym  9586  xrlttri3  9590  ge0addcl  9771  ge0mulcl  9772  ge0xaddcl  9773  expclzaplem  10324  expge0  10336  expge1  10337  hashfacen  10586  qredeu  11785  nn0gcdsq  11885  cnovex  12375  iscn2  12379  txuni  12442  txcn  12454