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-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:  biimprcd  159  elsn2g  3616  preqr1g  3753  opth1  4221  euotd  4239  tz7.2  4339  reusv3  4445  alxfr  4446  reuhypd  4456  ordsucim  4484  suc11g  4541  nlimsucg  4550  xpsspw  4723  funcnvuni  5267  fvmptdv2  5585  fsn  5668  fconst2g  5711  funfvima  5727  foco2  5733  isores3  5794  eusvobj2  5839  ovmpodv2  5986  ovelrn  6001  f1opw2  6055  suppssfv  6057  suppssov1  6058  nnmordi  6495  nnmord  6496  qsss  6572  eroveu  6604  th3qlem1  6615  mapsncnv  6673  elixpsn  6713  ixpsnf1o  6714  en1bg  6778  mapxpen  6826  en1eqsnbi  6926  updjud  7059  addnidpig  7298  enq0tr  7396  prcdnql  7446  prcunqu  7447  genipv  7471  genpelvl  7474  genpelvu  7475  distrlem5prl  7548  distrlem5pru  7549  aptiprlemu  7602  mulid1  7917  ltne  8004  cnegex  8097  creur  8875  creui  8876  cju  8877  nnsub  8917  un0addcl  9168  un0mulcl  9169  zaddcl  9252  elz2  9283  qmulz  9582  qre  9584  qnegcl  9595  elpqb  9608  xrltne  9770  xlesubadd  9840  iccid  9882  fzsn  10022  fzsuc2  10035  fz1sbc  10052  elfzp12  10055  modqmuladd  10322  bcval5  10697  bcpasc  10700  hashprg  10743  hashfzo  10757  shftlem  10780  replim  10823  sqrtsq  11008  absle  11053  maxabslemval  11172  negfi  11191  xrmaxiflemval  11213  summodclem2  11345  summodc  11346  zsumdc  11347  fsum3  11350  fsummulc2  11411  fsum00  11425  isumsplit  11454  prodmodclem2  11540  prodmodc  11541  zproddc  11542  fprodseq  11546  prodsnf  11555  fzo0dvdseq  11817  divalgmod  11886  gcdabs1  11944  dvdsgcd  11967  dvdsmulgcd  11980  lcmgcdeq  12037  isprm2lem  12070  dvdsprime  12076  coprm  12098  prmdvdsexpr  12104  rpexp  12107  phibndlem  12170  dfphi2  12174  hashgcdlem  12192  odzdvds  12199  nnoddn2prm  12214  pythagtriplem1  12219  pceulem  12248  pcqmul  12257  pcqcl  12260  pcxnn0cl  12264  pcxcl  12265  pcneg  12278  pcabs  12279  pcgcd1  12281  pcz  12285  pcprmpw2  12286  pcprmpw  12287  dvdsprmpweqle  12290  difsqpwdvds  12291  pcaddlem  12292  pcadd  12293  pcmpt  12295  pockthg  12309  4sqlem2  12341  4sqlem4  12344  mul4sq  12346  mnd1id  12680  0subm  12702  istopon  12805  eltg3  12851  tgidm  12868  restbasg  12962  tgrest  12963  tgcn  13002  cnconst  13028  lmss  13040  txbas  13052  txbasval  13061  upxp  13066  blssps  13221  blss  13222  metrest  13300  blssioo  13339  elcncf1di  13360  lgsmod  13721  lgsne0  13733  lgsdirnn0  13742  2sqlem2  13745  mul2sq  13746  2sqlem7  13751  bj-peano4  13990