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  597  limelon  4077  eldifpw  4149  ssonuni  4155  peano2  4236  limom  4254  elrnmpt1  4503  cnveqb  4694  cnveq0  4695  relcoi1  4767  ndmfvg  5120  ffvresb  5244  caovord3d  5585  poxp  5766  frec0g  5893  nnm0r  5964  nnacl  5965  nnacom  5969  nnaass  5970  nndi  5971  nnmass  5972  nnmsucr  5973  nnmcom  5974  brecop  6098  ecopovtrn  6105  ecopovtrng  6108  mulcmpblnq  6216  ordpipqqs  6222  mulcmpblnq0  6288  genpprecll  6357  genppreclu  6358  addcmpblnr  6480  ax1rid  6569  axpre-mulgt0  6579  cnegexlem1  6789  msqge0  7206  mulge0  7209  ltleap  7219  nnmulcl  7521  nnsub  7538  elnn0z  7835  ztri3or0  7863  nneoor  7908  xltnegi  8227  bj-om  8513  peano5set  8516  bj-inf2vnlem2  8543  bj-inf2vn  8546  bj-inf2vn2  8547