Theorem syl5ibrcom 157

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

Hypotheses

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

Assertion

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

Proof of Theorem syl5ibrcom

Step	Hyp	Ref	Expression
1		imbitrrid.1	. . 3 |- ( ph -> th )
2		imbitrrid.2	. . 3 |- ( ch -> ( ps <-> th ) )
3	1, 2	imbitrrid 156	. 2 |- ( ch -> ( ph -> ps ) )
4	3	com12 30	1 |- ( ph -> ( ch -> 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:  biimprcd  160  elsn2g  3625  preqr1g  3765  opth1  4234  euotd  4252  tz7.2  4352  reusv3  4458  alxfr  4459  reuhypd  4469  ordsucim  4497  suc11g  4554  nlimsucg  4563  xpsspw  4736  funcnvuni  5282  fvmptdv2  5602  fsn  5685  fconst2g  5728  funfvima  5744  foco2  5750  isores3  5811  eusvobj2  5856  ovmpodv2  6003  ovelrn  6018  f1opw2  6072  suppssfv  6074  suppssov1  6075  nnmordi  6512  nnmord  6513  qsss  6589  eroveu  6621  th3qlem1  6632  mapsncnv  6690  elixpsn  6730  ixpsnf1o  6731  en1bg  6795  mapxpen  6843  en1eqsnbi  6943  updjud  7076  addnidpig  7330  enq0tr  7428  prcdnql  7478  prcunqu  7479  genipv  7503  genpelvl  7506  genpelvu  7507  distrlem5prl  7580  distrlem5pru  7581  aptiprlemu  7634  mulrid  7949  ltne  8036  cnegex  8129  creur  8910  creui  8911  cju  8912  nnsub  8952  un0addcl  9203  un0mulcl  9204  zaddcl  9287  elz2  9318  qmulz  9617  qre  9619  qnegcl  9630  elpqb  9643  xrltne  9807  xlesubadd  9877  iccid  9919  fzsn  10059  fzsuc2  10072  fz1sbc  10089  elfzp12  10092  modqmuladd  10359  bcval5  10734  bcpasc  10737  hashprg  10779  hashfzo  10793  shftlem  10816  replim  10859  sqrtsq  11044  absle  11089  maxabslemval  11208  negfi  11227  xrmaxiflemval  11249  summodclem2  11381  summodc  11382  zsumdc  11383  fsum3  11386  fsummulc2  11447  fsum00  11461  isumsplit  11490  prodmodclem2  11576  prodmodc  11577  zproddc  11578  fprodseq  11582  prodsnf  11591  fzo0dvdseq  11853  divalgmod  11922  gcdabs1  11980  dvdsgcd  12003  dvdsmulgcd  12016  lcmgcdeq  12073  isprm2lem  12106  dvdsprime  12112  coprm  12134  prmdvdsexpr  12140  rpexp  12143  phibndlem  12206  dfphi2  12210  hashgcdlem  12228  odzdvds  12235  nnoddn2prm  12250  pythagtriplem1  12255  pceulem  12284  pcqmul  12293  pcqcl  12296  pcxnn0cl  12300  pcxcl  12301  pcneg  12314  pcabs  12315  pcgcd1  12317  pcz  12321  pcprmpw2  12322  pcprmpw  12323  dvdsprmpweqle  12326  difsqpwdvds  12327  pcaddlem  12328  pcadd  12329  pcmpt  12331  pockthg  12345  4sqlem2  12377  4sqlem4  12380  mul4sq  12382  mnd1id  12776  0subm  12799  mulgnn0p1  12922  mulgnn0ass  12946  dvreq1  13210  nzrunit  13228  istopon  13293  eltg3  13339  tgidm  13356  restbasg  13450  tgrest  13451  tgcn  13490  cnconst  13516  lmss  13528  txbas  13540  txbasval  13549  upxp  13554  blssps  13709  blss  13710  metrest  13788  blssioo  13827  elcncf1di  13848  lgsmod  14209  lgsne0  14221  lgsdirnn0  14230  2sqlem2  14233  mul2sq  14234  2sqlem7  14239  bj-peano4  14478