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  3844  opth1  4322  euotd  4341  tz7.2  4445  reusv3  4551  alxfr  4552  reuhypd  4562  ordsucim  4592  suc11g  4649  nlimsucg  4658  xpsspw  4831  funcnvuni  5390  fvmptdv2  5726  fsn  5809  fconst2g  5858  funfvima  5875  foco2  5883  isores3  5945  riotaeqimp  5985  eusvobj2  5993  ovmpodv2  6144  ovelrn  6160  f1opw2  6218  suppssfv  6220  suppssov1  6221  nnmordi  6670  nnmord  6671  qsss  6749  eroveu  6781  th3qlem1  6792  mapsncnv  6850  elixpsn  6890  ixpsnf1o  6891  en1bg  6960  pw2f1odclem  7003  mapxpen  7017  en1eqsnbi  7124  updjud  7257  addnidpig  7531  enq0tr  7629  prcdnql  7679  prcunqu  7680  genipv  7704  genpelvl  7707  genpelvu  7708  distrlem5prl  7781  distrlem5pru  7782  aptiprlemu  7835  mulrid  8151  ltne  8239  cnegex  8332  creur  9114  creui  9115  cju  9116  nnsub  9157  un0addcl  9410  un0mulcl  9411  zaddcl  9494  elz2  9526  qmulz  9826  qre  9828  qnegcl  9839  elpqb  9853  xrltne  10017  xlesubadd  10087  iccid  10129  fzsn  10270  fzsuc2  10283  fz1sbc  10300  elfzp12  10303  modqmuladd  10596  bcval5  10993  bcpasc  10996  hashprg  11038  hashfzo  11052  wrdl1s1  11171  cats1un  11261  swrdccat3blem  11279  shftlem  11335  replim  11378  sqrtsq  11563  absle  11608  maxabslemval  11727  negfi  11747  xrmaxiflemval  11769  summodclem2  11901  summodc  11902  zsumdc  11903  fsum3  11906  fsummulc2  11967  fsum00  11981  isumsplit  12010  prodmodclem2  12096  prodmodc  12097  zproddc  12098  fprodseq  12102  prodsnf  12111  fzo0dvdseq  12376  divalgmod  12446  gcdabs1  12518  dvdsgcd  12541  dvdsmulgcd  12554  lcmgcdeq  12613  isprm2lem  12646  dvdsprime  12652  coprm  12674  prmdvdsexpr  12680  rpexp  12683  phibndlem  12746  dfphi2  12750  hashgcdlem  12768  odzdvds  12776  nnoddn2prm  12791  pythagtriplem1  12796  pceulem  12825  pcqmul  12834  pcqcl  12837  pcxnn0cl  12841  pcxcl  12842  pcneg  12856  pcabs  12857  pcgcd1  12859  pcz  12863  pcprmpw2  12864  pcprmpw  12865  dvdsprmpweqle  12868  difsqpwdvds  12869  pcaddlem  12870  pcadd  12871  pcmpt  12874  pockthg  12888  4sqlem2  12920  4sqlem4  12923  mul4sq  12925  mnd1id  13497  0subm  13525  mulgnn0p1  13678  mulgnn0ass  13703  dvreq1  14114  nzrunit  14160  rrgeq0  14237  domneq0  14244  lmodfopnelem2  14297  lss1d  14355  lspsneq0  14398  znidom  14629  znunit  14631  znrrg  14632  istopon  14695  eltg3  14739  tgidm  14756  restbasg  14850  tgrest  14851  tgcn  14890  cnconst  14916  lmss  14928  txbas  14940  txbasval  14949  upxp  14954  blssps  15109  blss  15110  metrest  15188  blssioo  15235  elcncf1di  15261  elply2  15417  plyf  15419  dvdsppwf1o  15671  perfectlem2  15682  perfect  15683  lgsmod  15713  lgsne0  15725  lgsdirnn0  15734  gausslemma2dlem1a  15745  gausslemma2dlem6  15754  lgseisenlem2  15758  lgsquadlem1  15764  lgsquadlem2  15765  2lgslem1b  15776  2sqlem2  15802  mul2sq  15803  2sqlem7  15808  lpvtx  15887  usgredgop  15979  wlk1walkdom  16080  upgrwlkvtxedg  16085  bj-peano4  16342