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  416  stdcndc  840  reupick3  3412  difprsnss  3716  trin2  5000  imadiflem  5275  fnun  5302  fco  5361  f1co  5413  foco  5428  f1oun  5460  f1oco  5463  eqfunfv  5596  ftpg  5677  issmo  6264  tfrlem5  6290  ener  6753  domtr  6759  unen  6790  xpdom2  6805  mapen  6820  pm54.43  7154  axpre-lttrn  7833  axpre-mulgt0  7836  zmulcl  9252  qaddcl  9581  qmulcl  9583  rpaddcl  9621  rpmulcl  9622  rpdivcl  9623  xrltnsym  9737  xrlttri3  9741  ge0addcl  9925  ge0mulcl  9926  ge0xaddcl  9927  expclzaplem  10487  expge0  10499  expge1  10500  hashfacen  10758  qredeu  12038  nn0gcdsq  12141  mul4sq  12333  cnovex  12949  iscn2  12953  txuni  13016  txcn  13028  lgsne0  13692  mul2sq  13705