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  850  reupick3  3489  difprsnss  3806  trin2  5123  fundif  5368  imadiflem  5403  fnun  5432  fco  5494  f1co  5548  foco  5564  f1oun  5597  f1oco  5600  eqfunfv  5742  ftpg  5830  issmo  6445  tfrlem5  6471  ener  6944  domtr  6950  unen  6982  xpdom2  7003  mapen  7020  pm54.43  7379  axpre-lttrn  8087  axpre-mulgt0  8090  zmulcl  9516  qaddcl  9847  qmulcl  9849  rpaddcl  9890  rpmulcl  9891  rpdivcl  9892  xrltnsym  10006  xrlttri3  10010  ge0addcl  10194  ge0mulcl  10195  ge0xaddcl  10196  expclzaplem  10802  expge0  10814  expge1  10815  hashfacen  11076  qredeu  12640  nn0gcdsq  12743  mul4sq  12938  cnovex  14891  iscn2  14895  txuni  14958  txcn  14970  lgsne0  15738  mul2sq  15816