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  3700  preqr1g  3847  opth1  4326  euotd  4345  tz7.2  4449  reusv3  4555  alxfr  4556  reuhypd  4566  ordsucim  4596  suc11g  4653  nlimsucg  4662  xpsspw  4836  funcnvuni  5396  fvmptdv2  5732  fsn  5815  fconst2g  5864  funfvima  5881  foco2  5889  isores3  5951  riotaeqimp  5991  eusvobj2  5999  ovmpodv2  6150  ovelrn  6166  f1opw2  6224  suppssfv  6226  suppssov1  6227  nnmordi  6679  nnmord  6680  qsss  6758  eroveu  6790  th3qlem1  6801  mapsncnv  6859  elixpsn  6899  ixpsnf1o  6900  en1bg  6969  pw2f1odclem  7015  mapxpen  7029  en1eqsnbi  7142  updjud  7275  addnidpig  7549  enq0tr  7647  prcdnql  7697  prcunqu  7698  genipv  7722  genpelvl  7725  genpelvu  7726  distrlem5prl  7799  distrlem5pru  7800  aptiprlemu  7853  mulrid  8169  ltne  8257  cnegex  8350  creur  9132  creui  9133  cju  9134  nnsub  9175  un0addcl  9428  un0mulcl  9429  zaddcl  9512  elz2  9544  qmulz  9850  qre  9852  qnegcl  9863  elpqb  9877  xrltne  10041  xlesubadd  10111  iccid  10153  fzsn  10294  fzsuc2  10307  fz1sbc  10324  elfzp12  10327  modqmuladd  10621  bcval5  11018  bcpasc  11021  hashprg  11065  hashfzo  11079  wrdl1s1  11200  cats1un  11295  swrdccat3blem  11313  shftlem  11370  replim  11413  sqrtsq  11598  absle  11643  maxabslemval  11762  negfi  11782  xrmaxiflemval  11804  summodclem2  11936  summodc  11937  zsumdc  11938  fsum3  11941  fsummulc2  12002  fsum00  12016  isumsplit  12045  prodmodclem2  12131  prodmodc  12132  zproddc  12133  fprodseq  12137  prodsnf  12146  fzo0dvdseq  12411  divalgmod  12481  gcdabs1  12553  dvdsgcd  12576  dvdsmulgcd  12589  lcmgcdeq  12648  isprm2lem  12681  dvdsprime  12687  coprm  12709  prmdvdsexpr  12715  rpexp  12718  phibndlem  12781  dfphi2  12785  hashgcdlem  12803  odzdvds  12811  nnoddn2prm  12826  pythagtriplem1  12831  pceulem  12860  pcqmul  12869  pcqcl  12872  pcxnn0cl  12876  pcxcl  12877  pcneg  12891  pcabs  12892  pcgcd1  12894  pcz  12898  pcprmpw2  12899  pcprmpw  12900  dvdsprmpweqle  12903  difsqpwdvds  12904  pcaddlem  12905  pcadd  12906  pcmpt  12909  pockthg  12923  4sqlem2  12955  4sqlem4  12958  mul4sq  12960  mnd1id  13532  0subm  13560  mulgnn0p1  13713  mulgnn0ass  13738  dvreq1  14149  nzrunit  14195  rrgeq0  14272  domneq0  14279  lmodfopnelem2  14332  lss1d  14390  lspsneq0  14433  znidom  14664  znunit  14666  znrrg  14667  istopon  14730  eltg3  14774  tgidm  14791  restbasg  14885  tgrest  14886  tgcn  14925  cnconst  14951  lmss  14963  txbas  14975  txbasval  14984  upxp  14989  blssps  15144  blss  15145  metrest  15223  blssioo  15270  elcncf1di  15296  elply2  15452  plyf  15454  dvdsppwf1o  15706  perfectlem2  15717  perfect  15718  lgsmod  15748  lgsne0  15760  lgsdirnn0  15769  gausslemma2dlem1a  15780  gausslemma2dlem6  15789  lgseisenlem2  15793  lgsquadlem1  15799  lgsquadlem2  15800  2lgslem1b  15811  2sqlem2  15837  mul2sq  15838  2sqlem7  15843  lpvtx  15923  usgredgop  16017  vtxd0nedgbfi  16110  wlk1walkdom  16170  upgrwlkvtxedg  16175  clwwlkext2edg  16231  clwwlknonccat  16242  bj-peano4  16500