Theorem syl5ibr 145

Description: A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.) (Revised by NM, 22-Sep-2013.)

Hypotheses

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

Assertion

Ref	Expression
syl5ibr	⊢ (χ → (φ → ψ))

Proof of Theorem syl5ibr

Step	Hyp	Ref	Expression
1		syl5ibr.1	. 2 ⊢ (φ → θ)
2		syl5ibr.2	. . 3 ⊢ (χ → (ψ ↔ θ))
3	2	bicomd 129	. 2 ⊢ (χ → (θ ↔ ψ))
4	1, 3	syl5ib 143	1 ⊢ (χ → (φ → ψ))

Syntax hints:   → wi 4   ↔ 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:  syl5ibrcom  146  biimprd  147  nbn2  600  limelon  4081  eldifpw  4154  ssonuni  4160  peano2  4241  limom  4259  elrnmpt1  4508  cnveqb  4699  cnveq0  4700  relcoi1  4772  ndmfvg  5125  ffvresb  5249  caovord3d  5590  poxp  5771  frec0g  5898  nnm0r  5969  nnacl  5970  nnacom  5974  nnaass  5975  nndi  5976  nnmass  5977  nnmsucr  5978  nnmcom  5979  brecop  6103  ecopovtrn  6110  ecopovtrng  6113  mulcmpblnq  6221  ordpipqqs  6227  mulcmpblnq0  6293  genpprecll  6362  genppreclu  6363  addcmpblnr  6483  ax1rid  6570  axpre-mulgt0  6580  cnegexlem1  6788  bj-om  7355  peano5set  7358  bj-inf2vnlem2  7385  bj-inf2vn  7388  bj-inf2vn2  7389