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  3741  preqr1g  3889  opth1  4374  euotd  4393  tz7.2  4497  reusv3  4604  alxfr  4605  reuhypd  4615  ordsucim  4645  suc11g  4702  nlimsucg  4711  xpsspw  4885  funcnvuni  5448  fvmptdv2  5792  fsn  5874  fconst2g  5924  funfvima  5944  foco2  5953  isores3  6015  riotaeqimp  6057  eusvobj2  6065  ovmpodv2  6216  ovelrn  6232  f1opw2  6290  suppssov1  6293  suppssfvg  6497  nnmordi  6783  nnmord  6784  qsss  6862  eroveu  6894  th3qlem1  6905  mapsncnv  6971  elixpsn  7011  ixpsnf1o  7012  en1bg  7081  pw2f1odclem  7128  mapxpen  7142  mapunen  7145  en1eqsnbi  7260  updjud  7416  addnidpig  7697  enq0tr  7795  prcdnql  7845  prcunqu  7846  genipv  7870  genpelvl  7873  genpelvu  7874  distrlem5prl  7947  distrlem5pru  7948  aptiprlemu  8001  mulrid  8317  ltne  8404  cnegex  8498  creur  9283  creui  9284  cju  9285  nnsub  9326  un0addcl  9579  un0mulcl  9580  zaddcl  9667  elz2  9699  qmulz  10006  qre  10008  qnegcl  10019  elpqb  10033  xrltne  10198  xlesubadd  10268  iccid  10310  fzsn  10455  fzsuc2  10469  fz1sbc  10486  elfzp12  10489  modqmuladd  10786  bcval5  11184  bcpasc  11187  hashprg  11232  hashfzo  11246  wrdl1s1  11381  cats1un  11476  swrdccat3blem  11494  shftlem  11564  replim  11607  sqrtsq  11793  absle  11838  maxabslemval  11957  negfi  11977  xrmaxiflemval  11999  summodclem2  12132  summodc  12133  zsumdc  12134  fsum3  12137  fsummulc2  12198  fsum00  12212  isumsplit  12241  prodmodclem2  12327  prodmodc  12328  zproddc  12329  fprodseq  12333  prodsnf  12342  fzo0dvdseq  12607  divalgmod  12677  gcdabs1  12749  dvdsgcd  12772  dvdsmulgcd  12785  lcmgcdeq  12844  isprm2lem  12877  dvdsprime  12883  coprm  12905  prmdvdsexpr  12911  rpexp  12914  phibndlem  12977  dfphi2  12981  hashgcdlem  12999  odzdvds  13007  nnoddn2prm  13022  pythagtriplem1  13027  pceulem  13056  pcqmul  13065  pcqcl  13068  pcxnn0cl  13072  pcxcl  13073  pcneg  13087  pcabs  13088  pcgcd1  13090  pcz  13094  pcprmpw2  13095  pcprmpw  13096  dvdsprmpweqle  13099  difsqpwdvds  13100  pcaddlem  13101  pcadd  13102  pcmpt  13105  pockthg  13119  4sqlem2  13151  4sqlem4  13154  mul4sq  13156  ballotfilemfc0  13215  ballotfilemfcc  13216  mnd1id  13746  0subm  13774  mulgnn0p1  13919  mulgnn0ass  13944  dvreq1  14432  nzrunit  14478  rrgeq0  14556  domneq0  14564  lmodfopnelem2  14645  lss1d  14703  lspsneq0  14746  gsumfsum  14906  znidom  14975  znunit  14977  znrrg  14978  istopon  15097  eltg3  15141  tgidm  15158  restbasg  15252  tgrest  15253  tgcn  15292  cnconst  15318  lmss  15330  txbas  15342  txbasval  15351  upxp  15356  blssps  15511  blss  15512  metrest  15590  blssioo  15637  elcncf1di  15663  elply2  15819  plyf  15821  dvdsppwf1o  16086  perfectlem2  16097  perfect  16098  lgsmod  16128  lgsne0  16140  lgsdirnn0  16149  gausslemma2dlem1a  16160  gausslemma2dlem6  16169  lgseisenlem2  16173  lgsquadlem1  16179  lgsquadlem2  16180  2lgslem1b  16191  2sqlem2  16217  mul2sq  16218  2sqlem7  16223  lpvtx  16303  usgredgop  16397  uhgrspansubgrlem  16500  vtxd0nedgbfi  16523  wlk1walkdom  16583  upgrwlkvtxedg  16588  clwwlkext2edg  16646  clwwlknonccat  16657  bj-peano4  16964