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-mp 5  ax-1 6  ax-2 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  686  limelon  4316  eldifpw  4393  ssonuni  4399  onsucuni2  4474  peano2  4504  limom  4522  elrnmpt1  4785  cnveqb  4989  cnveq0  4990  relcoi1  5065  ndmfvg  5445  ffvresb  5576  caovord3d  5934  poxp  6122  nnm0r  6368  nnacl  6369  nnacom  6373  nnaass  6374  nndi  6375  nnmass  6376  nnmsucr  6377  nnmcom  6378  brecop  6512  ecopovtrn  6519  ecopovtrng  6522  elpm2r  6553  map0g  6575  fundmen  6693  mapxpen  6735  phpm  6752  f1vrnfibi  6826  elfir  6854  mulcmpblnq  7169  ordpipqqs  7175  mulcmpblnq0  7245  genpprecll  7315  genppreclu  7316  addcmpblnr  7540  ax1rid  7678  axpre-mulgt0  7688  cnegexlem1  7930  msqge0  8371  mulge0  8374  ltleap  8387  nnmulcl  8734  nnsub  8752  elnn0z  9060  ztri3or0  9089  nneoor  9146  uz11  9341  xltnegi  9611  frec2uzuzd  10168  seq3fveq2  10235  seq3shft2  10239  seq3split  10245  seq3caopr3  10247  seq3id2  10275  seq3homo  10276  m1expcl2  10308  expadd  10328  expmul  10331  faclbnd  10480  hashfzp1  10563  hashfacen  10572  seq3coll  10578  caucvgrelemcau  10745  recan  10874  rexanre  10985  fsumiun  11239  efexp  11377  dvdstr  11519  alzdvds  11541  zob  11577  gcdmultiplez  11698  dvdssq  11708  cncongr2  11774  elrestr  12117  restopn2  12341  txcn  12433  txlm  12437  isxms2  12610  bj-om  13124  bj-inf2vnlem2  13158  bj-inf2vn  13161  bj-inf2vn2  13162