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  846  reupick3  3435  difprsnss  3745  trin2  5038  imadiflem  5314  fnun  5341  fco  5400  f1co  5452  foco  5467  f1oun  5500  f1oco  5503  eqfunfv  5639  ftpg  5721  issmo  6314  tfrlem5  6340  ener  6806  domtr  6812  unen  6843  xpdom2  6858  mapen  6875  pm54.43  7220  axpre-lttrn  7914  axpre-mulgt0  7917  zmulcl  9337  qaddcl  9667  qmulcl  9669  rpaddcl  9709  rpmulcl  9710  rpdivcl  9711  xrltnsym  9825  xrlttri3  9829  ge0addcl  10013  ge0mulcl  10014  ge0xaddcl  10015  expclzaplem  10578  expge0  10590  expge1  10591  hashfacen  10851  qredeu  12132  nn0gcdsq  12235  mul4sq  12429  cnovex  14173  iscn2  14177  txuni  14240  txcn  14252  lgsne0  14917  mul2sq  14941