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  3656  preqr1g  3797  opth1  4270  euotd  4288  tz7.2  4390  reusv3  4496  alxfr  4497  reuhypd  4507  ordsucim  4537  suc11g  4594  nlimsucg  4603  xpsspw  4776  funcnvuni  5328  fvmptdv2  5654  fsn  5737  fconst2g  5780  funfvima  5797  foco2  5803  isores3  5865  eusvobj2  5911  ovmpodv2  6060  ovelrn  6076  f1opw2  6133  suppssfv  6135  suppssov1  6136  nnmordi  6583  nnmord  6584  qsss  6662  eroveu  6694  th3qlem1  6705  mapsncnv  6763  elixpsn  6803  ixpsnf1o  6804  en1bg  6868  pw2f1odclem  6904  mapxpen  6918  en1eqsnbi  7024  updjud  7157  addnidpig  7422  enq0tr  7520  prcdnql  7570  prcunqu  7571  genipv  7595  genpelvl  7598  genpelvu  7599  distrlem5prl  7672  distrlem5pru  7673  aptiprlemu  7726  mulrid  8042  ltne  8130  cnegex  8223  creur  9005  creui  9006  cju  9007  nnsub  9048  un0addcl  9301  un0mulcl  9302  zaddcl  9385  elz2  9416  qmulz  9716  qre  9718  qnegcl  9729  elpqb  9743  xrltne  9907  xlesubadd  9977  iccid  10019  fzsn  10160  fzsuc2  10173  fz1sbc  10190  elfzp12  10193  modqmuladd  10477  bcval5  10874  bcpasc  10877  hashprg  10919  hashfzo  10933  shftlem  11000  replim  11043  sqrtsq  11228  absle  11273  maxabslemval  11392  negfi  11412  xrmaxiflemval  11434  summodclem2  11566  summodc  11567  zsumdc  11568  fsum3  11571  fsummulc2  11632  fsum00  11646  isumsplit  11675  prodmodclem2  11761  prodmodc  11762  zproddc  11763  fprodseq  11767  prodsnf  11776  fzo0dvdseq  12041  divalgmod  12111  gcdabs1  12183  dvdsgcd  12206  dvdsmulgcd  12219  lcmgcdeq  12278  isprm2lem  12311  dvdsprime  12317  coprm  12339  prmdvdsexpr  12345  rpexp  12348  phibndlem  12411  dfphi2  12415  hashgcdlem  12433  odzdvds  12441  nnoddn2prm  12456  pythagtriplem1  12461  pceulem  12490  pcqmul  12499  pcqcl  12502  pcxnn0cl  12506  pcxcl  12507  pcneg  12521  pcabs  12522  pcgcd1  12524  pcz  12528  pcprmpw2  12529  pcprmpw  12530  dvdsprmpweqle  12533  difsqpwdvds  12534  pcaddlem  12535  pcadd  12536  pcmpt  12539  pockthg  12553  4sqlem2  12585  4sqlem4  12588  mul4sq  12590  mnd1id  13160  0subm  13188  mulgnn0p1  13341  mulgnn0ass  13366  dvreq1  13776  nzrunit  13822  rrgeq0  13899  domneq0  13906  lmodfopnelem2  13959  lss1d  14017  lspsneq0  14060  znidom  14291  znunit  14293  znrrg  14294  istopon  14357  eltg3  14401  tgidm  14418  restbasg  14512  tgrest  14513  tgcn  14552  cnconst  14578  lmss  14590  txbas  14602  txbasval  14611  upxp  14616  blssps  14771  blss  14772  metrest  14850  blssioo  14897  elcncf1di  14923  elply2  15079  plyf  15081  dvdsppwf1o  15333  perfectlem2  15344  perfect  15345  lgsmod  15375  lgsne0  15387  lgsdirnn0  15396  gausslemma2dlem1a  15407  gausslemma2dlem6  15416  lgseisenlem2  15420  lgsquadlem1  15426  lgsquadlem2  15427  2lgslem1b  15438  2sqlem2  15464  mul2sq  15465  2sqlem7  15470  bj-peano4  15709