Theorem syl5ibr 154

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 139	. 2 ⊢ (𝜒 → (𝜃 ↔ 𝜓))
4	1, 3	syl5ib 152	1 ⊢ (𝜒 → (𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  syl5ibrcom  155  biimprd  156  nbn2  645  limelon  4154  eldifpw  4226  ssonuni  4232  onsucuni2  4307  peano2  4336  limom  4354  elrnmpt1  4603  cnveqb  4796  cnveq0  4797  relcoi1  4869  ndmfvg  5225  ffvresb  5349  caovord3d  5691  poxp  5873  nnm0r  6081  nnacl  6082  nnacom  6086  nnaass  6087  nndi  6088  nnmass  6089  nnmsucr  6090  nnmcom  6091  brecop  6219  ecopovtrn  6226  ecopovtrng  6229  fundmen  6309  phpm  6351  f1vrnfibi  6394  mulcmpblnq  6558  ordpipqqs  6564  mulcmpblnq0  6634  genpprecll  6704  genppreclu  6705  addcmpblnr  6916  ax1rid  7043  axpre-mulgt0  7053  cnegexlem1  7283  msqge0  7716  mulge0  7719  ltleap  7730  nnmulcl  8060  nnsub  8077  elnn0z  8364  ztri3or0  8393  nneoor  8449  uz11  8641  xltnegi  8902  frec2uzuzd  9404  iseqss  9446  iseqfveq2  9448  iseqshft2  9452  iseqsplit  9458  iseqcaopr3  9460  iseqhomo  9468  m1expcl2  9498  expadd  9518  expmul  9521  faclbnd  9668  caucvgrelemcau  9866  recan  9995  rexanre  10106  dvdstr  10232  alzdvds  10254  zob  10291  gcdmultiplez  10410  dvdssq  10420  cncongr2  10486  bj-om  10732  bj-inf2vnlem2  10766  bj-inf2vn  10769  bj-inf2vn2  10770