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  5120  fundif  5365  imadiflem  5400  fnun  5429  fco  5491  f1co  5545  foco  5561  f1oun  5594  f1oco  5597  eqfunfv  5739  ftpg  5827  issmo  6440  tfrlem5  6466  ener  6939  domtr  6945  unen  6977  xpdom2  6998  mapen  7015  pm54.43  7371  axpre-lttrn  8079  axpre-mulgt0  8082  zmulcl  9508  qaddcl  9838  qmulcl  9840  rpaddcl  9881  rpmulcl  9882  rpdivcl  9883  xrltnsym  9997  xrlttri3  10001  ge0addcl  10185  ge0mulcl  10186  ge0xaddcl  10187  expclzaplem  10793  expge0  10805  expge1  10806  hashfacen  11066  qredeu  12627  nn0gcdsq  12730  mul4sq  12925  cnovex  14878  iscn2  14882  txuni  14945  txcn  14957  lgsne0  15725  mul2sq  15803