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  852  reupick3  3491  difprsnss  3812  trin2  5130  fundif  5376  imadiflem  5411  fnun  5440  fco  5502  f1co  5557  foco  5573  f1oun  5606  f1oco  5609  eqfunfv  5752  ftpg  5841  issmo  6459  tfrlem5  6485  ener  6958  domtr  6964  unen  6996  xpdom2  7020  mapen  7037  pm54.43  7400  axpre-lttrn  8109  axpre-mulgt0  8112  zmulcl  9538  qaddcl  9874  qmulcl  9876  rpaddcl  9917  rpmulcl  9918  rpdivcl  9919  xrltnsym  10033  xrlttri3  10037  ge0addcl  10221  ge0mulcl  10222  ge0xaddcl  10223  expclzaplem  10831  expge0  10843  expge1  10844  hashfacen  11106  qredeu  12692  nn0gcdsq  12795  mul4sq  12990  cnovex  14949  iscn2  14953  txuni  15016  txcn  15028  lgsne0  15796  mul2sq  15874