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	|- ( 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 139	. 2 |- ( ch -> ( th <-> ps ) )
4	1, 3	syl5ib 152	1 |- ( ch -> ( ph -> ps ) )

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  646  limelon  4162  eldifpw  4234  ssonuni  4240  onsucuni2  4315  peano2  4344  limom  4362  elrnmpt1  4613  cnveqb  4806  cnveq0  4807  relcoi1  4879  ndmfvg  5236  ffvresb  5360  caovord3d  5702  poxp  5884  nnm0r  6123  nnacl  6124  nnacom  6128  nnaass  6129  nndi  6130  nnmass  6131  nnmsucr  6132  nnmcom  6133  brecop  6262  ecopovtrn  6269  ecopovtrng  6272  fundmen  6353  phpm  6400  f1vrnfibi  6453  mulcmpblnq  6620  ordpipqqs  6626  mulcmpblnq0  6696  genpprecll  6766  genppreclu  6767  addcmpblnr  6978  ax1rid  7105  axpre-mulgt0  7115  cnegexlem1  7350  msqge0  7783  mulge0  7786  ltleap  7797  nnmulcl  8127  nnsub  8144  elnn0z  8445  ztri3or0  8474  nneoor  8530  uz11  8722  xltnegi  8978  frec2uzuzd  9484  iseqss  9541  iseqsst  9542  iseqfveq2  9544  iseqshft2  9548  iseqsplit  9554  iseqcaopr3  9556  iseqid2  9564  iseqhomo  9565  m1expcl2  9595  expadd  9615  expmul  9618  faclbnd  9765  caucvgrelemcau  10004  recan  10133  rexanre  10244  dvdstr  10377  alzdvds  10399  zob  10435  gcdmultiplez  10554  dvdssq  10564  cncongr2  10630  bj-om  10890  bj-inf2vnlem2  10924  bj-inf2vn  10927  bj-inf2vn2  10928