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  3505  difprsnss  3831  trin2  5153  fundif  5399  imadiflem  5434  fnun  5463  fco  5526  f1co  5584  foco  5600  f1oun  5633  f1oco  5636  eqfunfv  5779  ftpg  5867  issmo  6518  tfrlem5  6544  ener  7018  domtr  7024  unen  7057  xpdom2  7081  mapen  7098  pm54.43  7486  axpre-lttrn  8195  axpre-mulgt0  8198  zmulcl  9627  qaddcl  9963  qmulcl  9965  rpaddcl  10006  rpmulcl  10007  rpdivcl  10008  xrltnsym  10122  xrlttri3  10126  ge0addcl  10310  ge0mulcl  10311  ge0xaddcl  10312  expclzaplem  10921  expge0  10933  expge1  10934  hashfacen  11201  qredeu  12787  nn0gcdsq  12890  mul4sq  13085  cnovex  15048  iscn2  15052  txuni  15115  txcn  15127  lgsne0  15898  mul2sq  15976