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  687  limelon  4377  eldifpw  4455  ssonuni  4465  onsucuni2  4541  peano2  4572  limom  4591  elrnmpt1  4855  cnveqb  5059  cnveq0  5060  relcoi1  5135  ndmfvg  5517  ffvresb  5648  caovord3d  6012  poxp  6200  nnm0r  6447  nnacl  6448  nnacom  6452  nnaass  6453  nndi  6454  nnmass  6455  nnmsucr  6456  nnmcom  6457  brecop  6591  ecopovtrn  6598  ecopovtrng  6601  elpm2r  6632  map0g  6654  fundmen  6772  mapxpen  6814  phpm  6831  f1vrnfibi  6910  elfir  6938  mulcmpblnq  7309  ordpipqqs  7315  mulcmpblnq0  7385  genpprecll  7455  genppreclu  7456  addcmpblnr  7680  ax1rid  7818  axpre-mulgt0  7828  cnegexlem1  8073  msqge0  8514  mulge0  8517  ltleap  8530  nnmulcl  8878  nnsub  8896  elnn0z  9204  ztri3or0  9233  nneoor  9293  uz11  9488  xltnegi  9771  frec2uzuzd  10337  seq3fveq2  10404  seq3shft2  10408  seq3split  10414  seq3caopr3  10416  seq3id2  10444  seq3homo  10445  m1expcl2  10477  expadd  10497  expmul  10500  faclbnd  10654  hashfzp1  10737  hashfacen  10749  seq3coll  10755  caucvgrelemcau  10922  recan  11051  rexanre  11162  fsumiun  11418  efexp  11623  dvdstr  11768  alzdvds  11792  zob  11828  gcdmultiplez  11954  dvdssq  11964  cncongr2  12036  prmdiveq  12168  pythagtriplem2  12198  pcexp  12241  elrestr  12564  restopn2  12823  txcn  12915  txlm  12919  isxms2  13092  bj-om  13819  bj-inf2vnlem2  13853  bj-inf2vn  13856  bj-inf2vn2  13857