Theorem syl5ibrcom 156

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 155	. 2 |- ( ch -> ( ph -> ps ) )
4	3	com12 30	1 |- ( ph -> ( ch -> ps ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biimprcd  159  elsn2g  3481  preqr1g  3616  opth1  4072  euotd  4090  tz7.2  4190  reusv3  4295  alxfr  4296  reuhypd  4306  ordsucim  4330  suc11g  4386  nlimsucg  4395  xpsspw  4563  funcnvuni  5096  fvmptdv2  5405  fsn  5483  fconst2g  5526  funfvima  5540  foco2  5547  isores3  5608  eusvobj2  5652  ovmpt2dv2  5792  ovelrn  5807  f1opw2  5864  suppssfv  5866  suppssov1  5867  nnmordi  6289  nnmord  6290  qsss  6365  eroveu  6397  th3qlem1  6408  mapsncnv  6466  elixpsn  6506  ixpsnf1o  6507  en1bg  6571  mapxpen  6618  en1eqsnbi  6712  updjud  6827  addnidpig  6956  enq0tr  7054  prcdnql  7104  prcunqu  7105  genipv  7129  genpelvl  7132  genpelvu  7133  distrlem5prl  7206  distrlem5pru  7207  aptiprlemu  7260  mulid1  7546  ltne  7631  cnegex  7721  creur  8480  creui  8481  cju  8482  nnsub  8522  un0addcl  8767  un0mulcl  8768  zaddcl  8851  elz2  8879  qmulz  9169  qre  9171  qnegcl  9182  xrltne  9339  iccid  9404  fzsn  9541  fzsuc2  9554  fz1sbc  9571  elfzp12  9574  modqmuladd  9834  iseqid3  9998  ibcval5  10232  bcpasc  10235  hashprg  10277  hashfzo  10291  shftlem  10311  replim  10354  sqrtsq  10538  absle  10583  maxabslemval  10702  negfi  10720  isummolem2  10833  isummo  10834  zisum  10835  fisum  10839  fsummulc2  10903  fsum00  10917  isumsplit  10946  fzo0dvdseq  11197  divalgmod  11266  gcdabs1  11319  dvdsgcd  11340  dvdsmulgcd  11353  lcmgcdeq  11404  isprm2lem  11437  dvdsprime  11443  coprm  11462  prmdvdsexpr  11468  rpexp  11471  phibndlem  11531  dfphi2  11535  hashgcdlem  11542  istopon  11773  eltg3  11818  tgidm  11835  elcncf1di  11908  bj-peano4  12123