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  8467  creur  9250  creui  9251  cju  9252  nnsub  9293  un0addcl  9546  un0mulcl  9547  zaddcl  9634  elz2  9666  qmulz  9973  qre  9975  qnegcl  9986  elpqb  10000  xrltne  10165  xlesubadd  10235  iccid  10277  fzsn  10421  fzsuc2  10435  fz1sbc  10452  elfzp12  10455  modqmuladd  10752  bcval5  11150  bcpasc  11153  hashprg  11198  hashfzo  11212  wrdl1s1  11343  cats1un  11438  swrdccat3blem  11456  shftlem  11526  replim  11569  sqrtsq  11754  absle  11799  maxabslemval  11918  negfi  11938  xrmaxiflemval  11960  summodclem2  12093  summodc  12094  zsumdc  12095  fsum3  12098  fsummulc2  12159  fsum00  12173  isumsplit  12202  prodmodclem2  12288  prodmodc  12289  zproddc  12290  fprodseq  12294  prodsnf  12303  fzo0dvdseq  12568  divalgmod  12638  gcdabs1  12710  dvdsgcd  12733  dvdsmulgcd  12746  lcmgcdeq  12805  isprm2lem  12838  dvdsprime  12844  coprm  12866  prmdvdsexpr  12872  rpexp  12875  phibndlem  12938  dfphi2  12942  hashgcdlem  12960  odzdvds  12968  nnoddn2prm  12983  pythagtriplem1  12988  pceulem  13017  pcqmul  13026  pcqcl  13029  pcxnn0cl  13033  pcxcl  13034  pcneg  13048  pcabs  13049  pcgcd1  13051  pcz  13055  pcprmpw2  13056  pcprmpw  13057  dvdsprmpweqle  13060  difsqpwdvds  13061  pcaddlem  13062  pcadd  13063  pcmpt  13066  pockthg  13080  4sqlem2  13112  4sqlem4  13115  mul4sq  13117  ballotfilemfc0  13176  ballotfilemfcc  13177  mnd1id  13753  0subm  13781  mulgnn0p1  13934  mulgnn0ass  13959  dvreq1  14372  nzrunit  14418  rrgeq0  14496  domneq0  14504  lmodfopnelem2  14585  lss1d  14643  lspsneq0  14686  znidom  14917  znunit  14919  znrrg  14920  istopon  14990  eltg3  15034  tgidm  15051  restbasg  15145  tgrest  15146  tgcn  15185  cnconst  15211  lmss  15223  txbas  15235  txbasval  15244  upxp  15249  blssps  15404  blss  15405  metrest  15483  blssioo  15530  elcncf1di  15556  elply2  15712  plyf  15714  dvdsppwf1o  15969  perfectlem2  15980  perfect  15981  lgsmod  16011  lgsne0  16023  lgsdirnn0  16032  gausslemma2dlem1a  16043  gausslemma2dlem6  16052  lgseisenlem2  16056  lgsquadlem1  16062  lgsquadlem2  16063  2lgslem1b  16074  2sqlem2  16100  mul2sq  16101  2sqlem7  16106  lpvtx  16186  usgredgop  16280  uhgrspansubgrlem  16383  vtxd0nedgbfi  16406  wlk1walkdom  16466  upgrwlkvtxedg  16471  clwwlkext2edg  16529  clwwlknonccat  16540  bj-peano4  16837