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 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  sylancb  422  stdcndc  857  reupick3  3518  difprsnss  3853  trin2  5182  fundif  5428  imadiflem  5463  fnun  5492  fco  5555  f1co  5613  foco  5629  f1oun  5662  f1oco  5665  eqfunfv  5814  ftpg  5902  issmo  6563  tfrlem5  6589  ener  7071  domtr  7077  unen  7110  xpdom2  7134  mapen  7151  pm54.43  7543  axpre-lttrn  8258  axpre-mulgt0  8261  zmulcl  9710  qaddcl  10052  qmulcl  10054  rpaddcl  10096  rpmulcl  10097  rpdivcl  10098  xrltnsym  10213  xrlttri3  10217  ge0addcl  10401  ge0mulcl  10402  ge0xaddcl  10403  expclzaplem  11022  expge0  11034  expge1  11035  hashfacen  11307  qredeu  12901  nn0gcdsq  13006  mul4sq  13203  ballotfilem2  13287  cnovex  15434  iscn2  15438  txuni  15501  txcn  15513  efnnfsumcl  16251  efchtqdvds  16277  lgsne0  16374  mul2sq  16452