Theorem syl5ibr 156

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  syl5ibrcom  157  biimprd  158  nbn2  697  limelon  4393  eldifpw  4471  ssonuni  4481  onsucuni2  4557  peano2  4588  limom  4607  elrnmpt1  4871  cnveqb  5076  cnveq0  5077  relcoi1  5152  ndmfvg  5538  ffvresb  5671  caovord3d  6035  poxp  6223  nnm0r  6470  nnacl  6471  nnacom  6475  nnaass  6476  nndi  6477  nnmass  6478  nnmsucr  6479  nnmcom  6480  brecop  6615  ecopovtrn  6622  ecopovtrng  6625  elpm2r  6656  map0g  6678  fundmen  6796  mapxpen  6838  phpm  6855  f1vrnfibi  6934  elfir  6962  mulcmpblnq  7342  ordpipqqs  7348  mulcmpblnq0  7418  genpprecll  7488  genppreclu  7489  addcmpblnr  7713  ax1rid  7851  axpre-mulgt0  7861  cnegexlem1  8106  msqge0  8547  mulge0  8550  ltleap  8563  nnmulcl  8913  nnsub  8931  elnn0z  9239  ztri3or0  9268  nneoor  9328  uz11  9523  xltnegi  9806  frec2uzuzd  10372  seq3fveq2  10439  seq3shft2  10443  seq3split  10449  seq3caopr3  10451  seq3id2  10479  seq3homo  10480  m1expcl2  10512  expadd  10532  expmul  10535  faclbnd  10689  hashfzp1  10772  hashfacen  10784  seq3coll  10790  caucvgrelemcau  10957  recan  11086  rexanre  11197  fsumiun  11453  efexp  11658  dvdstr  11803  alzdvds  11827  zob  11863  gcdmultiplez  11989  dvdssq  11999  cncongr2  12071  prmdiveq  12203  pythagtriplem2  12233  pcexp  12276  elrestr  12627  dfgrp3me  12840  mulgneg2  12886  mulgnnass  12887  mhmmulg  12893  ringadd2  13016  mulgass2  13040  restopn2  13263  txcn  13355  txlm  13359  isxms2  13532  bj-om  14258  bj-inf2vnlem2  14292  bj-inf2vn  14295  bj-inf2vn2  14296