Theorem sylan2br 272

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)

Hypotheses

Ref	Expression
sylan2br.1	⊢ (𝜒 ↔ 𝜑)
sylan2br.2	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
sylan2br	⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Proof of Theorem sylan2br

Step	Hyp	Ref	Expression
1		sylan2br.1	. . 3 ⊢ (𝜒 ↔ 𝜑)
2	1	biimpri 124	. 2 ⊢ (𝜑 → 𝜒)
3		sylan2br.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan2 270	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  syl2anbr  276  xordc1  1284  imainss  4739  xpexr2m  4762  funeu2  4927  imadiflem  4978  fnop  5002  ssimaex  5234  isosolem  5463  acexmidlem2  5509  fnovex  5538  smores3  5908  riinerm  6179  enq0sym  6528  peano5nnnn  6964  axcaucvglemres  6971  uzind3  8349  xrltnsym  8712  0fz1  8907  iseqf  9198  expivallem  9230  expival  9231  exp1  9235  expp1  9236  resqrexlemf1  9580  resqrexlemfp1  9581  clim2iser  9831  clim2iser2  9832  iisermulc2  9834  iserile  9836  climserile  9839