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  613  limelon  4136  eldifpw  4208  ssonuni  4214  onsucuni2  4288  peano2  4318  limom  4336  elrnmpt1  4585  cnveqb  4776  cnveq0  4777  relcoi1  4849  ndmfvg  5204  ffvresb  5328  caovord3d  5671  poxp  5853  nnm0r  6058  nnacl  6059  nnacom  6063  nnaass  6064  nndi  6065  nnmass  6066  nnmsucr  6067  nnmcom  6068  brecop  6196  ecopovtrn  6203  ecopovtrng  6206  fundmen  6286  phpm  6327  mulcmpblnq  6466  ordpipqqs  6472  mulcmpblnq0  6542  genpprecll  6612  genppreclu  6613  addcmpblnr  6824  ax1rid  6951  axpre-mulgt0  6961  cnegexlem1  7186  msqge0  7607  mulge0  7610  ltleap  7621  nnmulcl  7935  nnsub  7952  elnn0z  8258  ztri3or0  8287  nneoor  8340  uz11  8495  xltnegi  8748  frec2uzuzd  9188  iseqss  9226  iseqfveq2  9228  iseqshft2  9232  iseqsplit  9238  iseqcaopr3  9240  iseqhomo  9248  m1expcl2  9277  expadd  9297  expmul  9300  caucvgrelemcau  9579  recan  9705  bj-om  10061  peano5setOLD  10065  bj-inf2vnlem2  10096  bj-inf2vn  10099  bj-inf2vn2  10100