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  3668  preqr1g  3810  opth1  4285  euotd  4304  tz7.2  4406  reusv3  4512  alxfr  4513  reuhypd  4523  ordsucim  4553  suc11g  4610  nlimsucg  4619  xpsspw  4792  funcnvuni  5349  fvmptdv2  5679  fsn  5762  fconst2g  5809  funfvima  5826  foco2  5832  isores3  5894  eusvobj2  5940  ovmpodv2  6089  ovelrn  6105  f1opw2  6162  suppssfv  6164  suppssov1  6165  nnmordi  6612  nnmord  6613  qsss  6691  eroveu  6723  th3qlem1  6734  mapsncnv  6792  elixpsn  6832  ixpsnf1o  6833  en1bg  6902  pw2f1odclem  6943  mapxpen  6957  en1eqsnbi  7063  updjud  7196  addnidpig  7462  enq0tr  7560  prcdnql  7610  prcunqu  7611  genipv  7635  genpelvl  7638  genpelvu  7639  distrlem5prl  7712  distrlem5pru  7713  aptiprlemu  7766  mulrid  8082  ltne  8170  cnegex  8263  creur  9045  creui  9046  cju  9047  nnsub  9088  un0addcl  9341  un0mulcl  9342  zaddcl  9425  elz2  9457  qmulz  9757  qre  9759  qnegcl  9770  elpqb  9784  xrltne  9948  xlesubadd  10018  iccid  10060  fzsn  10201  fzsuc2  10214  fz1sbc  10231  elfzp12  10234  modqmuladd  10524  bcval5  10921  bcpasc  10924  hashprg  10966  hashfzo  10980  wrdl1s1  11098  shftlem  11177  replim  11220  sqrtsq  11405  absle  11450  maxabslemval  11569  negfi  11589  xrmaxiflemval  11611  summodclem2  11743  summodc  11744  zsumdc  11745  fsum3  11748  fsummulc2  11809  fsum00  11823  isumsplit  11852  prodmodclem2  11938  prodmodc  11939  zproddc  11940  fprodseq  11944  prodsnf  11953  fzo0dvdseq  12218  divalgmod  12288  gcdabs1  12360  dvdsgcd  12383  dvdsmulgcd  12396  lcmgcdeq  12455  isprm2lem  12488  dvdsprime  12494  coprm  12516  prmdvdsexpr  12522  rpexp  12525  phibndlem  12588  dfphi2  12592  hashgcdlem  12610  odzdvds  12618  nnoddn2prm  12633  pythagtriplem1  12638  pceulem  12667  pcqmul  12676  pcqcl  12679  pcxnn0cl  12683  pcxcl  12684  pcneg  12698  pcabs  12699  pcgcd1  12701  pcz  12705  pcprmpw2  12706  pcprmpw  12707  dvdsprmpweqle  12710  difsqpwdvds  12711  pcaddlem  12712  pcadd  12713  pcmpt  12716  pockthg  12730  4sqlem2  12762  4sqlem4  12765  mul4sq  12767  mnd1id  13338  0subm  13366  mulgnn0p1  13519  mulgnn0ass  13544  dvreq1  13954  nzrunit  14000  rrgeq0  14077  domneq0  14084  lmodfopnelem2  14137  lss1d  14195  lspsneq0  14238  znidom  14469  znunit  14471  znrrg  14472  istopon  14535  eltg3  14579  tgidm  14596  restbasg  14690  tgrest  14691  tgcn  14730  cnconst  14756  lmss  14768  txbas  14780  txbasval  14789  upxp  14794  blssps  14949  blss  14950  metrest  15028  blssioo  15075  elcncf1di  15101  elply2  15257  plyf  15259  dvdsppwf1o  15511  perfectlem2  15522  perfect  15523  lgsmod  15553  lgsne0  15565  lgsdirnn0  15574  gausslemma2dlem1a  15585  gausslemma2dlem6  15594  lgseisenlem2  15598  lgsquadlem1  15604  lgsquadlem2  15605  2lgslem1b  15616  2sqlem2  15642  mul2sq  15643  2sqlem7  15648  lpvtx  15725  bj-peano4  16005