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  422  stdcndc  857  reupick3  3518  difprsnss  3851  trin2  5177  fundif  5423  imadiflem  5458  fnun  5487  fco  5550  f1co  5608  foco  5624  f1oun  5657  f1oco  5660  eqfunfv  5805  ftpg  5893  issmo  6553  tfrlem5  6579  ener  7060  domtr  7066  unen  7099  xpdom2  7123  mapen  7140  pm54.43  7530  axpre-lttrn  8245  axpre-mulgt0  8248  zmulcl  9681  qaddcl  10018  qmulcl  10020  rpaddcl  10061  rpmulcl  10062  rpdivcl  10063  xrltnsym  10178  xrlttri3  10182  ge0addcl  10366  ge0mulcl  10367  ge0xaddcl  10368  expclzaplem  10983  expge0  10995  expge1  10996  hashfacen  11267  qredeu  12858  nn0gcdsq  12961  mul4sq  13156  ballotfilem2  13211  cnovex  15280  iscn2  15284  txuni  15347  txcn  15359  lgsne0  16140  mul2sq  16218