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  3766  opth1  4236  euotd  4254  tz7.2  4354  reusv3  4460  alxfr  4461  reuhypd  4471  ordsucim  4499  suc11g  4556  nlimsucg  4565  xpsspw  4738  funcnvuni  5285  fvmptdv2  5605  fsn  5688  fconst2g  5731  funfvima  5748  foco2  5754  isores3  5815  eusvobj2  5860  ovmpodv2  6007  ovelrn  6022  f1opw2  6076  suppssfv  6078  suppssov1  6079  nnmordi  6516  nnmord  6517  qsss  6593  eroveu  6625  th3qlem1  6636  mapsncnv  6694  elixpsn  6734  ixpsnf1o  6735  en1bg  6799  mapxpen  6847  en1eqsnbi  6947  updjud  7080  addnidpig  7334  enq0tr  7432  prcdnql  7482  prcunqu  7483  genipv  7507  genpelvl  7510  genpelvu  7511  distrlem5prl  7584  distrlem5pru  7585  aptiprlemu  7638  mulrid  7953  ltne  8041  cnegex  8134  creur  8915  creui  8916  cju  8917  nnsub  8957  un0addcl  9208  un0mulcl  9209  zaddcl  9292  elz2  9323  qmulz  9622  qre  9624  qnegcl  9635  elpqb  9648  xrltne  9812  xlesubadd  9882  iccid  9924  fzsn  10065  fzsuc2  10078  fz1sbc  10095  elfzp12  10098  modqmuladd  10365  bcval5  10742  bcpasc  10745  hashprg  10787  hashfzo  10801  shftlem  10824  replim  10867  sqrtsq  11052  absle  11097  maxabslemval  11216  negfi  11235  xrmaxiflemval  11257  summodclem2  11389  summodc  11390  zsumdc  11391  fsum3  11394  fsummulc2  11455  fsum00  11469  isumsplit  11498  prodmodclem2  11584  prodmodc  11585  zproddc  11586  fprodseq  11590  prodsnf  11599  fzo0dvdseq  11862  divalgmod  11931  gcdabs1  11989  dvdsgcd  12012  dvdsmulgcd  12025  lcmgcdeq  12082  isprm2lem  12115  dvdsprime  12121  coprm  12143  prmdvdsexpr  12149  rpexp  12152  phibndlem  12215  dfphi2  12219  hashgcdlem  12237  odzdvds  12244  nnoddn2prm  12259  pythagtriplem1  12264  pceulem  12293  pcqmul  12302  pcqcl  12305  pcxnn0cl  12309  pcxcl  12310  pcneg  12323  pcabs  12324  pcgcd1  12326  pcz  12330  pcprmpw2  12331  pcprmpw  12332  dvdsprmpweqle  12335  difsqpwdvds  12336  pcaddlem  12337  pcadd  12338  pcmpt  12340  pockthg  12354  4sqlem2  12386  4sqlem4  12389  mul4sq  12391  mnd1id  12847  0subm  12870  mulgnn0p1  12993  mulgnn0ass  13017  dvreq1  13309  nzrunit  13327  istopon  13483  eltg3  13527  tgidm  13544  restbasg  13638  tgrest  13639  tgcn  13678  cnconst  13704  lmss  13716  txbas  13728  txbasval  13737  upxp  13742  blssps  13897  blss  13898  metrest  13976  blssioo  14015  elcncf1di  14036  lgsmod  14397  lgsne0  14409  lgsdirnn0  14418  lgseisenlem2  14421  2sqlem2  14432  mul2sq  14433  2sqlem7  14438  bj-peano4  14677