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  612  limelon  4102  eldifpw  4174  ssonuni  4180  peano2  4261  limom  4279  elrnmpt1  4528  cnveqb  4719  cnveq0  4720  relcoi1  4792  ndmfvg  5147  ffvresb  5271  caovord3d  5613  poxp  5794  nnm0r  5997  nnacl  5998  nnacom  6002  nnaass  6003  nndi  6004  nnmass  6005  nnmsucr  6006  nnmcom  6007  brecop  6132  ecopovtrn  6139  ecopovtrng  6142  fundmen  6222  mulcmpblnq  6352  ordpipqqs  6358  mulcmpblnq0  6427  genpprecll  6497  genppreclu  6498  addcmpblnr  6667  ax1rid  6761  axpre-mulgt0  6771  cnegexlem1  6983  msqge0  7400  mulge0  7403  ltleap  7413  nnmulcl  7716  nnsub  7733  elnn0z  8034  ztri3or0  8063  nneoor  8116  uz11  8271  xltnegi  8518  frec2uzuzd  8869  iseqfveq2  8905  m1expcl2  8931  expadd  8951  expmul  8954  bj-om  9396  peano5setOLD  9400  bj-inf2vnlem2  9431  bj-inf2vn  9434  bj-inf2vn2  9435