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  3699  preqr1g  3843  opth1  4321  euotd  4340  tz7.2  4442  reusv3  4548  alxfr  4549  reuhypd  4559  ordsucim  4589  suc11g  4646  nlimsucg  4655  xpsspw  4828  funcnvuni  5386  fvmptdv2  5717  fsn  5800  fconst2g  5847  funfvima  5864  foco2  5870  isores3  5932  riotaeqimp  5972  eusvobj2  5980  ovmpodv2  6129  ovelrn  6145  f1opw2  6202  suppssfv  6204  suppssov1  6205  nnmordi  6652  nnmord  6653  qsss  6731  eroveu  6763  th3qlem1  6774  mapsncnv  6832  elixpsn  6872  ixpsnf1o  6873  en1bg  6942  pw2f1odclem  6983  mapxpen  6997  en1eqsnbi  7104  updjud  7237  addnidpig  7511  enq0tr  7609  prcdnql  7659  prcunqu  7660  genipv  7684  genpelvl  7687  genpelvu  7688  distrlem5prl  7761  distrlem5pru  7762  aptiprlemu  7815  mulrid  8131  ltne  8219  cnegex  8312  creur  9094  creui  9095  cju  9096  nnsub  9137  un0addcl  9390  un0mulcl  9391  zaddcl  9474  elz2  9506  qmulz  9806  qre  9808  qnegcl  9819  elpqb  9833  xrltne  9997  xlesubadd  10067  iccid  10109  fzsn  10250  fzsuc2  10263  fz1sbc  10280  elfzp12  10283  modqmuladd  10575  bcval5  10972  bcpasc  10975  hashprg  11017  hashfzo  11031  wrdl1s1  11149  cats1un  11239  swrdccat3blem  11257  shftlem  11313  replim  11356  sqrtsq  11541  absle  11586  maxabslemval  11705  negfi  11725  xrmaxiflemval  11747  summodclem2  11879  summodc  11880  zsumdc  11881  fsum3  11884  fsummulc2  11945  fsum00  11959  isumsplit  11988  prodmodclem2  12074  prodmodc  12075  zproddc  12076  fprodseq  12080  prodsnf  12089  fzo0dvdseq  12354  divalgmod  12424  gcdabs1  12496  dvdsgcd  12519  dvdsmulgcd  12532  lcmgcdeq  12591  isprm2lem  12624  dvdsprime  12630  coprm  12652  prmdvdsexpr  12658  rpexp  12661  phibndlem  12724  dfphi2  12728  hashgcdlem  12746  odzdvds  12754  nnoddn2prm  12769  pythagtriplem1  12774  pceulem  12803  pcqmul  12812  pcqcl  12815  pcxnn0cl  12819  pcxcl  12820  pcneg  12834  pcabs  12835  pcgcd1  12837  pcz  12841  pcprmpw2  12842  pcprmpw  12843  dvdsprmpweqle  12846  difsqpwdvds  12847  pcaddlem  12848  pcadd  12849  pcmpt  12852  pockthg  12866  4sqlem2  12898  4sqlem4  12901  mul4sq  12903  mnd1id  13475  0subm  13503  mulgnn0p1  13656  mulgnn0ass  13681  dvreq1  14091  nzrunit  14137  rrgeq0  14214  domneq0  14221  lmodfopnelem2  14274  lss1d  14332  lspsneq0  14375  znidom  14606  znunit  14608  znrrg  14609  istopon  14672  eltg3  14716  tgidm  14733  restbasg  14827  tgrest  14828  tgcn  14867  cnconst  14893  lmss  14905  txbas  14917  txbasval  14926  upxp  14931  blssps  15086  blss  15087  metrest  15165  blssioo  15212  elcncf1di  15238  elply2  15394  plyf  15396  dvdsppwf1o  15648  perfectlem2  15659  perfect  15660  lgsmod  15690  lgsne0  15702  lgsdirnn0  15711  gausslemma2dlem1a  15722  gausslemma2dlem6  15731  lgseisenlem2  15735  lgsquadlem1  15741  lgsquadlem2  15742  2lgslem1b  15753  2sqlem2  15779  mul2sq  15780  2sqlem7  15785  lpvtx  15864  usgredgop  15956  bj-peano4  16248