Theorem syl5ibrcom 157

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

Hypotheses

Ref	Expression
imbitrrid.1	⊢ (𝜑 → 𝜃)
imbitrrid.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
syl5ibrcom	⊢ (𝜑 → (𝜒 → 𝜓))

Proof of Theorem syl5ibrcom

Step	Hyp	Ref	Expression
1		imbitrrid.1	. . 3 ⊢ (𝜑 → 𝜃)
2		imbitrrid.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	1, 2	imbitrrid 156	. 2 ⊢ (𝜒 → (𝜑 → 𝜓))
4	3	com12 30	1 ⊢ (𝜑 → (𝜒 → 𝜓))

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  3727  preqr1g  3875  opth1  4357  euotd  4376  tz7.2  4480  reusv3  4586  alxfr  4587  reuhypd  4597  ordsucim  4627  suc11g  4684  nlimsucg  4693  xpsspw  4867  funcnvuni  5430  fvmptdv2  5772  fsn  5854  fconst2g  5904  funfvima  5923  foco2  5932  isores3  5994  riotaeqimp  6036  eusvobj2  6044  ovmpodv2  6195  ovelrn  6211  f1opw2  6269  suppssov1  6272  suppssfvg  6476  nnmordi  6762  nnmord  6763  qsss  6841  eroveu  6873  th3qlem1  6884  mapsncnv  6943  elixpsn  6983  ixpsnf1o  6984  en1bg  7053  pw2f1odclem  7100  mapxpen  7114  mapunen  7117  en1eqsnbi  7232  updjud  7386  addnidpig  7667  enq0tr  7765  prcdnql  7815  prcunqu  7816  genipv  7840  genpelvl  7843  genpelvu  7844  distrlem5prl  7917  distrlem5pru  7918  aptiprlemu  7971  mulrid  8287  ltne  8374  cnegex  8468  creur  9253  creui  9254  cju  9255  nnsub  9296  un0addcl  9549  un0mulcl  9550  zaddcl  9637  elz2  9669  qmulz  9976  qre  9978  qnegcl  9989  elpqb  10003  xrltne  10168  xlesubadd  10238  iccid  10280  fzsn  10424  fzsuc2  10438  fz1sbc  10455  elfzp12  10458  modqmuladd  10755  bcval5  11153  bcpasc  11156  hashprg  11201  hashfzo  11215  wrdl1s1  11346  cats1un  11441  swrdccat3blem  11459  shftlem  11529  replim  11572  sqrtsq  11758  absle  11803  maxabslemval  11922  negfi  11942  xrmaxiflemval  11964  summodclem2  12097  summodc  12098  zsumdc  12099  fsum3  12102  fsummulc2  12163  fsum00  12177  isumsplit  12206  prodmodclem2  12292  prodmodc  12293  zproddc  12294  fprodseq  12298  prodsnf  12307  fzo0dvdseq  12572  divalgmod  12642  gcdabs1  12714  dvdsgcd  12737  dvdsmulgcd  12750  lcmgcdeq  12809  isprm2lem  12842  dvdsprime  12848  coprm  12870  prmdvdsexpr  12876  rpexp  12879  phibndlem  12942  dfphi2  12946  hashgcdlem  12964  odzdvds  12972  nnoddn2prm  12987  pythagtriplem1  12992  pceulem  13021  pcqmul  13030  pcqcl  13033  pcxnn0cl  13037  pcxcl  13038  pcneg  13052  pcabs  13053  pcgcd1  13055  pcz  13059  pcprmpw2  13060  pcprmpw  13061  dvdsprmpweqle  13064  difsqpwdvds  13065  pcaddlem  13066  pcadd  13067  pcmpt  13070  pockthg  13084  4sqlem2  13116  4sqlem4  13119  mul4sq  13121  ballotfilemfc0  13180  ballotfilemfcc  13181  mnd1id  13715  0subm  13743  mulgnn0p1  13890  mulgnn0ass  13915  dvreq1  14391  nzrunit  14437  rrgeq0  14515  domneq0  14523  lmodfopnelem2  14603  lss1d  14661  lspsneq0  14704  znidom  14935  znunit  14937  znrrg  14938  istopon  15008  eltg3  15052  tgidm  15069  restbasg  15163  tgrest  15164  tgcn  15203  cnconst  15229  lmss  15241  txbas  15253  txbasval  15262  upxp  15267  blssps  15422  blss  15423  metrest  15501  blssioo  15548  elcncf1di  15574  elply2  15730  plyf  15732  dvdsppwf1o  15987  perfectlem2  15998  perfect  15999  lgsmod  16029  lgsne0  16041  lgsdirnn0  16050  gausslemma2dlem1a  16061  gausslemma2dlem6  16070  lgseisenlem2  16074  lgsquadlem1  16080  lgsquadlem2  16081  2lgslem1b  16092  2sqlem2  16118  mul2sq  16119  2sqlem7  16124  lpvtx  16204  usgredgop  16298  uhgrspansubgrlem  16401  vtxd0nedgbfi  16424  wlk1walkdom  16484  upgrwlkvtxedg  16489  clwwlkext2edg  16547  clwwlknonccat  16558  bj-peano4  16865