Theorem syl5ibrcom 155

Description: A mixed syllogism inference. (Contributed by NM, 20-Jun-2007.)

Hypotheses

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

Assertion

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

Proof of Theorem syl5ibrcom

Step	Hyp	Ref	Expression
1		syl5ibr.1	. . 3 |- ( ph -> th )
2		syl5ibr.2	. . 3 |- ( ch -> ( ps <-> th ) )
3	1, 2	syl5ibr 154	. 2 |- ( ch -> ( ph -> ps ) )
4	3	com12 30	1 |- ( ph -> ( ch -> 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:  biimprcd  158  elsn2g  3477  preqr1g  3610  opth1  4063  euotd  4081  tz7.2  4181  reusv3  4282  alxfr  4283  reuhypd  4293  ordsucim  4317  suc11g  4373  nlimsucg  4382  xpsspw  4550  funcnvuni  5083  fvmptdv2  5392  fsn  5469  fconst2g  5512  funfvima  5526  foco2  5533  isores3  5594  eusvobj2  5638  ovmpt2dv2  5778  ovelrn  5793  f1opw2  5850  suppssfv  5852  suppssov1  5853  nnmordi  6273  nnmord  6274  qsss  6349  eroveu  6381  th3qlem1  6392  mapsncnv  6450  en1bg  6515  mapxpen  6562  en1eqsnbi  6656  updjud  6771  addnidpig  6893  enq0tr  6991  prcdnql  7041  prcunqu  7042  genipv  7066  genpelvl  7069  genpelvu  7070  distrlem5prl  7143  distrlem5pru  7144  aptiprlemu  7197  mulid1  7483  ltne  7568  cnegex  7658  creur  8417  creui  8418  cju  8419  nnsub  8459  un0addcl  8704  un0mulcl  8705  zaddcl  8788  elz2  8816  qmulz  9106  qre  9108  qnegcl  9119  xrltne  9276  iccid  9341  fzsn  9477  fzsuc2  9489  fz1sbc  9506  elfzp12  9509  modqmuladd  9769  iseqid3  9933  ibcval5  10167  bcpasc  10170  hashprg  10212  hashfzo  10226  shftlem  10246  replim  10289  sqrtsq  10473  absle  10518  maxabslemval  10637  negfi  10655  isummolem2  10768  isummo  10769  zisum  10770  fisum  10774  fsummulc2  10838  fsum00  10852  isumsplit  10881  fzo0dvdseq  11132  divalgmod  11201  gcdabs1  11254  dvdsgcd  11275  dvdsmulgcd  11288  lcmgcdeq  11339  isprm2lem  11372  dvdsprime  11378  coprm  11397  prmdvdsexpr  11403  rpexp  11406  phibndlem  11466  dfphi2  11470  hashgcdlem  11477  istopon  11565  elcncf1di  11590  bj-peano4  11805