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  3492  difprsnss  3811  trin2  5128  fundif  5374  imadiflem  5409  fnun  5438  fco  5500  f1co  5554  foco  5570  f1oun  5603  f1oco  5606  eqfunfv  5749  ftpg  5838  issmo  6454  tfrlem5  6480  ener  6953  domtr  6959  unen  6991  xpdom2  7015  mapen  7032  pm54.43  7395  axpre-lttrn  8104  axpre-mulgt0  8107  zmulcl  9533  qaddcl  9869  qmulcl  9871  rpaddcl  9912  rpmulcl  9913  rpdivcl  9914  xrltnsym  10028  xrlttri3  10032  ge0addcl  10216  ge0mulcl  10217  ge0xaddcl  10218  expclzaplem  10826  expge0  10838  expge1  10839  hashfacen  11101  qredeu  12671  nn0gcdsq  12774  mul4sq  12969  cnovex  14923  iscn2  14927  txuni  14990  txcn  15002  lgsne0  15770  mul2sq  15848