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  3706  preqr1g  3854  opth1  4334  euotd  4353  tz7.2  4457  reusv3  4563  alxfr  4564  reuhypd  4574  ordsucim  4604  suc11g  4661  nlimsucg  4670  xpsspw  4844  funcnvuni  5406  fvmptdv2  5745  fsn  5827  fconst2g  5877  funfvima  5896  foco2  5904  isores3  5966  riotaeqimp  6006  eusvobj2  6014  ovmpodv2  6165  ovelrn  6181  f1opw2  6239  suppssov1  6241  suppssfvg  6441  nnmordi  6727  nnmord  6728  qsss  6806  eroveu  6838  th3qlem1  6849  mapsncnv  6907  elixpsn  6947  ixpsnf1o  6948  en1bg  7017  pw2f1odclem  7063  mapxpen  7077  en1eqsnbi  7191  updjud  7324  addnidpig  7599  enq0tr  7697  prcdnql  7747  prcunqu  7748  genipv  7772  genpelvl  7775  genpelvu  7776  distrlem5prl  7849  distrlem5pru  7850  aptiprlemu  7903  mulrid  8219  ltne  8307  cnegex  8400  creur  9182  creui  9183  cju  9184  nnsub  9225  un0addcl  9478  un0mulcl  9479  zaddcl  9562  elz2  9594  qmulz  9900  qre  9902  qnegcl  9913  elpqb  9927  xrltne  10091  xlesubadd  10161  iccid  10203  fzsn  10344  fzsuc2  10357  fz1sbc  10374  elfzp12  10377  modqmuladd  10672  bcval5  11069  bcpasc  11072  hashprg  11116  hashfzo  11130  wrdl1s1  11254  cats1un  11349  swrdccat3blem  11367  shftlem  11437  replim  11480  sqrtsq  11665  absle  11710  maxabslemval  11829  negfi  11849  xrmaxiflemval  11871  summodclem2  12004  summodc  12005  zsumdc  12006  fsum3  12009  fsummulc2  12070  fsum00  12084  isumsplit  12113  prodmodclem2  12199  prodmodc  12200  zproddc  12201  fprodseq  12205  prodsnf  12214  fzo0dvdseq  12479  divalgmod  12549  gcdabs1  12621  dvdsgcd  12644  dvdsmulgcd  12657  lcmgcdeq  12716  isprm2lem  12749  dvdsprime  12755  coprm  12777  prmdvdsexpr  12783  rpexp  12786  phibndlem  12849  dfphi2  12853  hashgcdlem  12871  odzdvds  12879  nnoddn2prm  12894  pythagtriplem1  12899  pceulem  12928  pcqmul  12937  pcqcl  12940  pcxnn0cl  12944  pcxcl  12945  pcneg  12959  pcabs  12960  pcgcd1  12962  pcz  12966  pcprmpw2  12967  pcprmpw  12968  dvdsprmpweqle  12971  difsqpwdvds  12972  pcaddlem  12973  pcadd  12974  pcmpt  12977  pockthg  12991  4sqlem2  13023  4sqlem4  13026  mul4sq  13028  mnd1id  13600  0subm  13628  mulgnn0p1  13781  mulgnn0ass  13806  dvreq1  14218  nzrunit  14264  rrgeq0  14341  domneq0  14348  lmodfopnelem2  14401  lss1d  14459  lspsneq0  14502  znidom  14733  znunit  14735  znrrg  14736  istopon  14804  eltg3  14848  tgidm  14865  restbasg  14959  tgrest  14960  tgcn  14999  cnconst  15025  lmss  15037  txbas  15049  txbasval  15058  upxp  15063  blssps  15218  blss  15219  metrest  15297  blssioo  15344  elcncf1di  15370  elply2  15526  plyf  15528  dvdsppwf1o  15783  perfectlem2  15794  perfect  15795  lgsmod  15825  lgsne0  15837  lgsdirnn0  15846  gausslemma2dlem1a  15857  gausslemma2dlem6  15866  lgseisenlem2  15870  lgsquadlem1  15876  lgsquadlem2  15877  2lgslem1b  15888  2sqlem2  15914  mul2sq  15915  2sqlem7  15920  lpvtx  16000  usgredgop  16094  uhgrspansubgrlem  16197  vtxd0nedgbfi  16220  wlk1walkdom  16280  upgrwlkvtxedg  16285  clwwlkext2edg  16343  clwwlknonccat  16354  bj-peano4  16651