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  3655  preqr1g  3796  opth1  4269  euotd  4287  tz7.2  4389  reusv3  4495  alxfr  4496  reuhypd  4506  ordsucim  4536  suc11g  4593  nlimsucg  4602  xpsspw  4775  funcnvuni  5327  fvmptdv2  5651  fsn  5734  fconst2g  5777  funfvima  5794  foco2  5800  isores3  5862  eusvobj2  5908  ovmpodv2  6056  ovelrn  6072  f1opw2  6129  suppssfv  6131  suppssov1  6132  nnmordi  6574  nnmord  6575  qsss  6653  eroveu  6685  th3qlem1  6696  mapsncnv  6754  elixpsn  6794  ixpsnf1o  6795  en1bg  6859  pw2f1odclem  6895  mapxpen  6909  en1eqsnbi  7015  updjud  7148  addnidpig  7403  enq0tr  7501  prcdnql  7551  prcunqu  7552  genipv  7576  genpelvl  7579  genpelvu  7580  distrlem5prl  7653  distrlem5pru  7654  aptiprlemu  7707  mulrid  8023  ltne  8111  cnegex  8204  creur  8986  creui  8987  cju  8988  nnsub  9029  un0addcl  9282  un0mulcl  9283  zaddcl  9366  elz2  9397  qmulz  9697  qre  9699  qnegcl  9710  elpqb  9724  xrltne  9888  xlesubadd  9958  iccid  10000  fzsn  10141  fzsuc2  10154  fz1sbc  10171  elfzp12  10174  modqmuladd  10458  bcval5  10855  bcpasc  10858  hashprg  10900  hashfzo  10914  shftlem  10981  replim  11024  sqrtsq  11209  absle  11254  maxabslemval  11373  negfi  11393  xrmaxiflemval  11415  summodclem2  11547  summodc  11548  zsumdc  11549  fsum3  11552  fsummulc2  11613  fsum00  11627  isumsplit  11656  prodmodclem2  11742  prodmodc  11743  zproddc  11744  fprodseq  11748  prodsnf  11757  fzo0dvdseq  12022  divalgmod  12092  gcdabs1  12156  dvdsgcd  12179  dvdsmulgcd  12192  lcmgcdeq  12251  isprm2lem  12284  dvdsprime  12290  coprm  12312  prmdvdsexpr  12318  rpexp  12321  phibndlem  12384  dfphi2  12388  hashgcdlem  12406  odzdvds  12414  nnoddn2prm  12429  pythagtriplem1  12434  pceulem  12463  pcqmul  12472  pcqcl  12475  pcxnn0cl  12479  pcxcl  12480  pcneg  12494  pcabs  12495  pcgcd1  12497  pcz  12501  pcprmpw2  12502  pcprmpw  12503  dvdsprmpweqle  12506  difsqpwdvds  12507  pcaddlem  12508  pcadd  12509  pcmpt  12512  pockthg  12526  4sqlem2  12558  4sqlem4  12561  mul4sq  12563  mnd1id  13088  0subm  13116  mulgnn0p1  13263  mulgnn0ass  13288  dvreq1  13698  nzrunit  13744  rrgeq0  13821  domneq0  13828  lmodfopnelem2  13881  lss1d  13939  lspsneq0  13982  znidom  14213  znunit  14215  znrrg  14216  istopon  14249  eltg3  14293  tgidm  14310  restbasg  14404  tgrest  14405  tgcn  14444  cnconst  14470  lmss  14482  txbas  14494  txbasval  14503  upxp  14508  blssps  14663  blss  14664  metrest  14742  blssioo  14789  elcncf1di  14815  elply2  14971  plyf  14973  dvdsppwf1o  15225  perfectlem2  15236  perfect  15237  lgsmod  15267  lgsne0  15279  lgsdirnn0  15288  gausslemma2dlem1a  15299  gausslemma2dlem6  15308  lgseisenlem2  15312  lgsquadlem1  15318  lgsquadlem2  15319  2lgslem1b  15330  2sqlem2  15356  mul2sq  15357  2sqlem7  15362  bj-peano4  15601