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  3721  preqr1g  3869  opth1  4351  euotd  4370  tz7.2  4474  reusv3  4580  alxfr  4581  reuhypd  4591  ordsucim  4621  suc11g  4678  nlimsucg  4687  xpsspw  4861  funcnvuni  5424  fvmptdv2  5766  fsn  5848  fconst2g  5898  funfvima  5917  foco2  5925  isores3  5987  riotaeqimp  6027  eusvobj2  6035  ovmpodv2  6186  ovelrn  6202  f1opw2  6260  suppssov1  6262  suppssfvg  6462  nnmordi  6748  nnmord  6749  qsss  6827  eroveu  6859  th3qlem1  6870  mapsncnv  6929  elixpsn  6969  ixpsnf1o  6970  en1bg  7039  pw2f1odclem  7086  mapxpen  7100  mapunen  7103  en1eqsnbi  7218  updjud  7372  addnidpig  7650  enq0tr  7748  prcdnql  7798  prcunqu  7799  genipv  7823  genpelvl  7826  genpelvu  7827  distrlem5prl  7900  distrlem5pru  7901  aptiprlemu  7954  mulrid  8270  ltne  8357  cnegex  8450  creur  9232  creui  9233  cju  9234  nnsub  9275  un0addcl  9528  un0mulcl  9529  zaddcl  9616  elz2  9648  qmulz  9954  qre  9956  qnegcl  9967  elpqb  9981  xrltne  10145  xlesubadd  10215  iccid  10257  fzsn  10399  fzsuc2  10412  fz1sbc  10429  elfzp12  10432  modqmuladd  10727  bcval5  11124  bcpasc  11127  hashprg  11171  hashfzo  11185  wrdl1s1  11314  cats1un  11409  swrdccat3blem  11427  shftlem  11497  replim  11540  sqrtsq  11725  absle  11770  maxabslemval  11889  negfi  11909  xrmaxiflemval  11931  summodclem2  12064  summodc  12065  zsumdc  12066  fsum3  12069  fsummulc2  12130  fsum00  12144  isumsplit  12173  prodmodclem2  12259  prodmodc  12260  zproddc  12261  fprodseq  12265  prodsnf  12274  fzo0dvdseq  12539  divalgmod  12609  gcdabs1  12681  dvdsgcd  12704  dvdsmulgcd  12717  lcmgcdeq  12776  isprm2lem  12809  dvdsprime  12815  coprm  12837  prmdvdsexpr  12843  rpexp  12846  phibndlem  12909  dfphi2  12913  hashgcdlem  12931  odzdvds  12939  nnoddn2prm  12954  pythagtriplem1  12959  pceulem  12988  pcqmul  12997  pcqcl  13000  pcxnn0cl  13004  pcxcl  13005  pcneg  13019  pcabs  13020  pcgcd1  13022  pcz  13026  pcprmpw2  13027  pcprmpw  13028  dvdsprmpweqle  13031  difsqpwdvds  13032  pcaddlem  13033  pcadd  13034  pcmpt  13037  pockthg  13051  4sqlem2  13083  4sqlem4  13086  mul4sq  13088  mnd1id  13661  0subm  13689  mulgnn0p1  13842  mulgnn0ass  13867  dvreq1  14279  nzrunit  14325  rrgeq0  14402  domneq0  14410  lmodfopnelem2  14465  lss1d  14523  lspsneq0  14566  znidom  14797  znunit  14799  znrrg  14800  istopon  14870  eltg3  14914  tgidm  14931  restbasg  15025  tgrest  15026  tgcn  15065  cnconst  15091  lmss  15103  txbas  15115  txbasval  15124  upxp  15129  blssps  15284  blss  15285  metrest  15363  blssioo  15410  elcncf1di  15436  elply2  15592  plyf  15594  dvdsppwf1o  15849  perfectlem2  15860  perfect  15861  lgsmod  15891  lgsne0  15903  lgsdirnn0  15912  gausslemma2dlem1a  15923  gausslemma2dlem6  15932  lgseisenlem2  15936  lgsquadlem1  15942  lgsquadlem2  15943  2lgslem1b  15954  2sqlem2  15980  mul2sq  15981  2sqlem7  15986  lpvtx  16066  usgredgop  16160  uhgrspansubgrlem  16263  vtxd0nedgbfi  16286  wlk1walkdom  16346  upgrwlkvtxedg  16351  clwwlkext2edg  16409  clwwlknonccat  16420  bj-peano4  16717