Theorem sylbir 204

Description: A mixed syllogism inference from a biconditional and an implication. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
sylbir.1	⊢ (ψ ↔ φ)
sylbir.2	⊢ (ψ → χ)

Assertion

Ref	Expression
sylbir	⊢ (φ → χ)

Proof of Theorem sylbir

Step	Hyp	Ref	Expression
1		sylbir.1	. . 3 ⊢ (ψ ↔ φ)
2	1	biimpri 197	. 2 ⊢ (φ → ψ)
3		sylbir.2	. 2 ⊢ (ψ → χ)
4	2, 3	syl 15	1 ⊢ (φ → χ)

Syntax hints:   → wi 4   ↔ wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  3imtr3i  256  ex  423  3ori  1242  19.38  1794  ax12olem5  1931  sbi2  2064  sb5rf  2090  ax11eq  2193  ax11el  2194  mo  2226  mo2  2233  2mo  2282  axie2  2329  bm1.1  2338  necon1i  2561  sbhypf  2905  vtocl2  2911  vtocl3  2912  reu6  3026  uneqin  3507  inelcm  3606  difin0ss  3617  difprsn1  3848  unissint  3951  intminss  3953  iununi  4051  pw10b  4167  iotanul  4355  peano5  4410  elsuci  4415  nndisjeq  4430  nnceleq  4431  tfin11  4494  sfinltfin  4536  copsex2g  4610  opelopabsb  4698  opelopabt  4700  opelrn  4962  elimasn  5020  xpnz  5046  ssxpb  5056  funcnvres2  5168  tz6.12  5346  fnfvrnss  5430  fressnfv  5440  fconst5  5456  fconstfv  5457  ovidig  5594  ovres  5603  ovconst2  5612  oprssdm  5613  ndmovcl  5615  fvfullfun  5865  ecopqsi  5982  ncaddccl  6145  nceleq  6150  dflec3  6222  lenc  6224  letc  6232