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  4376  euotd  4395  tz7.2  4499  reusv3  4606  alxfr  4607  reuhypd  4617  ordsucim  4647  suc11g  4704  nlimsucg  4713  xpsspw  4887  funcnvuni  5450  fvmptdv2  5795  fsn  5880  fconst2g  5930  funfvima  5950  foco2  5959  isores3  6021  riotaeqimp  6063  eusvobj2  6071  ovmpodv2  6222  ovelrn  6238  f1opw2  6296  suppssov1  6299  suppssfvg  6503  nnmordi  6789  nnmord  6790  qsss  6868  eroveu  6900  th3qlem1  6911  mapsncnv  6977  elixpsn  7017  ixpsnf1o  7018  en1bg  7087  pw2f1odclem  7134  mapxpen  7148  mapunen  7151  en1eqsnbi  7266  updjud  7423  addnidpig  7704  enq0tr  7802  prcdnql  7852  prcunqu  7853  genipv  7877  genpelvl  7880  genpelvu  7881  distrlem5prl  7954  distrlem5pru  7955  aptiprlemu  8008  mulrid  8324  ltne  8411  cnegex  8506  creur  9292  creui  9293  cju  9294  nnsub  9346  un0addcl  9601  un0mulcl  9602  zaddcl  9689  elz2  9721  qmulz  10033  qre  10035  qnegcl  10046  elpqb  10061  xrltne  10226  xlesubadd  10296  iccid  10338  fzsn  10483  fzsuc2  10497  fz1sbc  10514  elfzp12  10517  modqmuladd  10818  bcval5  11217  bcpasc  11220  hashprg  11265  hashfzo  11279  wrdl1s1  11414  cats1un  11509  swrdccat3blem  11527  shftlem  11597  replim  11640  sqrtsq  11826  absle  11872  maxabslemval  11991  negfi  12011  xrmaxiflemval  12035  summodclem2  12168  summodc  12169  zsumdc  12170  fsum3  12173  fsummulc2  12234  fsum00  12248  isumsplit  12277  prodmodclem2  12363  prodmodc  12364  zproddc  12365  fprodseq  12369  prodsnf  12378  fzo0dvdseq  12643  divalgmod  12713  gcdabs1  12785  dvdsgcd  12808  dvdsmulgcd  12821  lcmgcdeq  12880  isprm2lem  12913  dvdsprime  12919  coprm  12942  prmdvdsexpr  12948  rpexp  12951  phibndlem  13017  dfphi2  13021  hashgcdlem  13039  odzdvds  13047  nnoddn2prm  13062  pythagtriplem1  13067  pceulem  13096  pcqmul  13105  pcqcl  13108  pcxnn0cl  13112  pcxcl  13113  pcneg  13127  pcabs  13128  pcgcd1  13130  pcz  13134  pcprmpw2  13135  pcprmpw  13136  dvdsprmpweqle  13139  difsqpwdvds  13140  pcaddlem  13141  pcadd  13142  pcmpt  13145  pockthg  13159  4sqlem2  13191  4sqlem4  13194  mul4sq  13196  prmlem1a  13244  ballotfilemfc0  13284  ballotfilemfcc  13285  mnd1id  13816  0subm  13844  mulgnn0p1  13989  mulgnn0ass  14014  dvreq1  14533  nzrunit  14579  rrgeq0  14657  domneq0  14665  lmodfopnelem2  14746  lss1d  14804  lspsneq0  14847  gsumfsum  15007  znidom  15076  znunit  15078  znrrg  15079  istopon  15205  eltg3  15249  tgidm  15266  restbasg  15360  tgrest  15361  tgcn  15400  cnconst  15426  lmss  15438  txbas  15450  txbasval  15459  upxp  15464  blssps  15619  blss  15620  metrest  15698  blssioo  15745  elcncf1di  15771  elply2  15927  plyf  15929  dvdsppwf1o  16244  ppiublem1  16252  chtublem  16256  perfectlem2  16261  perfect  16262  bposlem1  16272  lgsmod  16311  lgsne0  16323  lgsdirnn0  16332  gausslemma2dlem1a  16343  gausslemma2dlem6  16352  lgseisenlem2  16356  lgsquadlem1  16362  lgsquadlem2  16363  2lgslem1b  16374  2sqlem2  16400  mul2sq  16401  2sqlem7  16406  lpvtx  16486  usgredgop  16580  uhgrspansubgrlem  16683  vtxd0nedgbfi  16706  wlk1walkdom  16766  upgrwlkvtxedg  16771  clwwlkext2edg  16829  clwwlknonccat  16840  bj-peano4  17147