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  4323  euotd  4342  tz7.2  4446  reusv3  4552  alxfr  4553  reuhypd  4563  ordsucim  4593  suc11g  4650  nlimsucg  4659  xpsspw  4833  funcnvuni  5393  fvmptdv2  5729  fsn  5812  fconst2g  5861  funfvima  5878  foco2  5886  isores3  5948  riotaeqimp  5988  eusvobj2  5996  ovmpodv2  6147  ovelrn  6163  f1opw2  6221  suppssfv  6223  suppssov1  6224  nnmordi  6675  nnmord  6676  qsss  6754  eroveu  6786  th3qlem1  6797  mapsncnv  6855  elixpsn  6895  ixpsnf1o  6896  en1bg  6965  pw2f1odclem  7008  mapxpen  7022  en1eqsnbi  7132  updjud  7265  addnidpig  7539  enq0tr  7637  prcdnql  7687  prcunqu  7688  genipv  7712  genpelvl  7715  genpelvu  7716  distrlem5prl  7789  distrlem5pru  7790  aptiprlemu  7843  mulrid  8159  ltne  8247  cnegex  8340  creur  9122  creui  9123  cju  9124  nnsub  9165  un0addcl  9418  un0mulcl  9419  zaddcl  9502  elz2  9534  qmulz  9835  qre  9837  qnegcl  9848  elpqb  9862  xrltne  10026  xlesubadd  10096  iccid  10138  fzsn  10279  fzsuc2  10292  fz1sbc  10309  elfzp12  10312  modqmuladd  10605  bcval5  11002  bcpasc  11005  hashprg  11048  hashfzo  11062  wrdl1s1  11183  cats1un  11274  swrdccat3blem  11292  shftlem  11348  replim  11391  sqrtsq  11576  absle  11621  maxabslemval  11740  negfi  11760  xrmaxiflemval  11782  summodclem2  11914  summodc  11915  zsumdc  11916  fsum3  11919  fsummulc2  11980  fsum00  11994  isumsplit  12023  prodmodclem2  12109  prodmodc  12110  zproddc  12111  fprodseq  12115  prodsnf  12124  fzo0dvdseq  12389  divalgmod  12459  gcdabs1  12531  dvdsgcd  12554  dvdsmulgcd  12567  lcmgcdeq  12626  isprm2lem  12659  dvdsprime  12665  coprm  12687  prmdvdsexpr  12693  rpexp  12696  phibndlem  12759  dfphi2  12763  hashgcdlem  12781  odzdvds  12789  nnoddn2prm  12804  pythagtriplem1  12809  pceulem  12838  pcqmul  12847  pcqcl  12850  pcxnn0cl  12854  pcxcl  12855  pcneg  12869  pcabs  12870  pcgcd1  12872  pcz  12876  pcprmpw2  12877  pcprmpw  12878  dvdsprmpweqle  12881  difsqpwdvds  12882  pcaddlem  12883  pcadd  12884  pcmpt  12887  pockthg  12901  4sqlem2  12933  4sqlem4  12936  mul4sq  12938  mnd1id  13510  0subm  13538  mulgnn0p1  13691  mulgnn0ass  13716  dvreq1  14127  nzrunit  14173  rrgeq0  14250  domneq0  14257  lmodfopnelem2  14310  lss1d  14368  lspsneq0  14411  znidom  14642  znunit  14644  znrrg  14645  istopon  14708  eltg3  14752  tgidm  14769  restbasg  14863  tgrest  14864  tgcn  14903  cnconst  14929  lmss  14941  txbas  14953  txbasval  14962  upxp  14967  blssps  15122  blss  15123  metrest  15201  blssioo  15248  elcncf1di  15274  elply2  15430  plyf  15432  dvdsppwf1o  15684  perfectlem2  15695  perfect  15696  lgsmod  15726  lgsne0  15738  lgsdirnn0  15747  gausslemma2dlem1a  15758  gausslemma2dlem6  15767  lgseisenlem2  15771  lgsquadlem1  15777  lgsquadlem2  15778  2lgslem1b  15789  2sqlem2  15815  mul2sq  15816  2sqlem7  15821  lpvtx  15900  usgredgop  15992  vtxd0nedgbfi  16085  wlk1walkdom  16131  upgrwlkvtxedg  16136  clwwlkext2edg  16190  bj-peano4  16427