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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  biimprcd  160  elsn2g  3742  preqr1g  3891  opth1  4378  euotd  4397  tz7.2  4501  reusv3  4608  alxfr  4609  reuhypd  4619  ordsucim  4649  suc11g  4706  nlimsucg  4715  xpsspw  4889  funcnvuni  5453  fvmptdv2  5798  fsn  5883  fconst2g  5933  funfvima  5953  foco2  5962  isores3  6024  riotaeqimp  6066  eusvobj2  6074  ovmpodv2  6225  ovelrn  6241  f1opw2  6299  suppssov1  6302  suppssfvg  6507  nnmordi  6793  nnmord  6794  qsss  6872  eroveu  6904  th3qlem1  6915  mapsncnv  6981  elixpsn  7021  ixpsnf1o  7022  en1bg  7091  pw2f1odclem  7138  mapxpen  7152  mapunen  7155  en1eqsnbi  7271  updjud  7428  addnidpig  7709  enq0tr  7807  prcdnql  7857  prcunqu  7858  genipv  7882  genpelvl  7885  genpelvu  7886  distrlem5prl  7959  distrlem5pru  7960  aptiprlemu  8013  mulrid  8329  ltne  8416  cnegex  8511  creur  9297  creui  9298  cju  9299  nnsub  9352  un0addcl  9607  un0mulcl  9608  zaddcl  9695  elz2  9727  qmulz  10039  qre  10041  qnegcl  10052  elpqb  10067  xrltne  10232  xlesubadd  10302  iccid  10344  fzsn  10489  fzsuc2  10503  fz1sbc  10520  elfzp12  10523  modqmuladd  10824  bcval5  11223  bcpasc  11226  hashprg  11271  hashfzo  11285  wrdl1s1  11420  cats1un  11515  swrdccat3blem  11533  shftlem  11603  replim  11646  sqrtsq  11832  absle  11878  maxabslemval  11997  negfi  12017  xrmaxiflemval  12041  summodclem2  12174  summodc  12175  zsumdc  12176  fsum3  12179  fsummulc2  12240  fsum00  12254  isumsplit  12283  prodmodclem2  12369  prodmodc  12370  zproddc  12371  fprodseq  12375  prodsnf  12384  fzo0dvdseq  12649  divalgmod  12719  gcdabs1  12791  dvdsgcd  12814  dvdsmulgcd  12827  lcmgcdeq  12886  isprm2lem  12919  dvdsprime  12925  coprm  12948  prmdvdsexpr  12954  rpexp  12957  phibndlem  13023  dfphi2  13027  hashgcdlem  13045  odzdvds  13053  nnoddn2prm  13068  pythagtriplem1  13073  pceulem  13102  pcqmul  13111  pcqcl  13114  pcxnn0cl  13118  pcxcl  13119  pcneg  13133  pcabs  13134  pcgcd1  13136  pcz  13140  pcprmpw2  13141  pcprmpw  13142  dvdsprmpweqle  13145  difsqpwdvds  13146  pcaddlem  13147  pcadd  13148  pcmpt  13151  pockthg  13165  4sqlem2  13197  4sqlem4  13200  mul4sq  13202  prmlem1a  13250  ballotfilemfc0  13290  ballotfilemfcc  13291  mnd1id  13822  0subm  13850  mulgnn0p1  13995  mulgnn0ass  14020  dvreq1  14558  nzrunit  14604  rrgeq0  14682  domneq0  14690  lmodfopnelem2  14771  lss1d  14829  lspsneq0  14872  gsumfsum  15032  znidom  15101  znunit  15103  znrrg  15104  istopon  15239  eltg3  15283  tgidm  15300  restbasg  15394  tgrest  15395  tgcn  15434  cnconst  15460  lmss  15472  txbas  15484  txbasval  15493  upxp  15498  blssps  15653  blss  15654  metrest  15732  blssioo  15779  elcncf1di  15805  elply2  15961  plyf  15963  efnthr  16176  dvdsppwf1o  16283  ppiublem1  16291  chtublem  16295  perfectlem2  16300  perfect  16301  bposlem1  16311  lgsmod  16350  lgsne0  16362  lgsdirnn0  16371  gausslemma2dlem1a  16382  gausslemma2dlem6  16391  lgseisenlem2  16395  lgsquadlem1  16401  lgsquadlem2  16402  2lgslem1b  16413  2sqlem2  16439  mul2sq  16440  2sqlem7  16445  lpvtx  16525  usgredgop  16619  uhgrspansubgrlem  16722  vtxd0nedgbfi  16745  wlk1walkdom  16805  upgrwlkvtxedg  16810  clwwlkext2edg  16868  clwwlknonccat  16879  bj-peano4  17186