Theorem syl5ibr 155

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

Hypotheses

Ref	Expression
syl5ibr.1	|- ( ph -> th )
syl5ibr.2	|- ( ch -> ( ps <-> th ) )

Assertion

Ref	Expression
syl5ibr	|- ( ch -> ( ph -> ps ) )

Proof of Theorem syl5ibr

Step	Hyp	Ref	Expression
1		syl5ibr.1	. 2 |- ( ph -> th )
2		syl5ibr.2	. . 3 |- ( ch -> ( ps <-> th ) )
3	2	bicomd 140	. 2 |- ( ch -> ( th <-> ps ) )
4	1, 3	syl5ib 153	1 |- ( ch -> ( ph -> ps ) )

Syntax hints:   -> wi 4   <-> wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  syl5ibrcom  156  biimprd  157  nbn2  669  limelon  4281  eldifpw  4358  ssonuni  4364  onsucuni2  4439  peano2  4469  limom  4487  elrnmpt1  4750  cnveqb  4952  cnveq0  4953  relcoi1  5028  ndmfvg  5406  ffvresb  5537  caovord3d  5895  poxp  6083  nnm0r  6329  nnacl  6330  nnacom  6334  nnaass  6335  nndi  6336  nnmass  6337  nnmsucr  6338  nnmcom  6339  brecop  6473  ecopovtrn  6480  ecopovtrng  6483  elpm2r  6514  map0g  6536  fundmen  6654  mapxpen  6695  phpm  6712  f1vrnfibi  6785  elfir  6813  mulcmpblnq  7124  ordpipqqs  7130  mulcmpblnq0  7200  genpprecll  7270  genppreclu  7271  addcmpblnr  7482  ax1rid  7612  axpre-mulgt0  7622  cnegexlem1  7860  msqge0  8296  mulge0  8299  ltleap  8311  nnmulcl  8651  nnsub  8669  elnn0z  8971  ztri3or0  9000  nneoor  9057  uz11  9250  xltnegi  9511  frec2uzuzd  10068  seq3fveq2  10135  seq3shft2  10139  seq3split  10145  seq3caopr3  10147  seq3id2  10175  seq3homo  10176  m1expcl2  10208  expadd  10228  expmul  10231  faclbnd  10380  hashfzp1  10463  hashfacen  10472  seq3coll  10478  caucvgrelemcau  10644  recan  10773  rexanre  10884  fsumiun  11138  efexp  11239  dvdstr  11378  alzdvds  11400  zob  11436  gcdmultiplez  11555  dvdssq  11565  cncongr2  11631  elrestr  11971  restopn2  12195  txcn  12286  txlm  12290  isxms2  12441  bj-om  12827  bj-inf2vnlem2  12861  bj-inf2vn  12864  bj-inf2vn2  12865