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  2560  sbhypf  2904  vtocl2  2910  vtocl3  2911  reu6  3025  uneqin  3506  inelcm  3605  difin0ss  3616  difprsn1  3847  unissint  3950  intminss  3952  iununi  4050  pw10b  4166  iotanul  4354  peano5  4409  elsuci  4414  nndisjeq  4429  nnceleq  4430  tfin11  4493  sfinltfin  4535  copsex2g  4609  opelopabsb  4697  opelopabt  4699  opelrn  4961  elimasn  5019  xpnz  5045  ssxpb  5055  funcnvres2  5167  tz6.12  5345  fnfvrnss  5429  fressnfv  5439  fconst5  5455  fconstfv  5456  ovidig  5593  ovres  5602  ovconst2  5611  oprssdm  5612  ndmovcl  5614  fvfullfun  5864  ecopqsi  5981  ncaddccl  6144  nceleq  6149  dflec3  6221  lenc  6223  letc  6231