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 ⊢ (𝜑 → (𝜒 → 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  biimprcd  160  elsn2g  3742  preqr1g  3891  opth1  4376  euotd  4395  tz7.2  4499  reusv3  4606  alxfr  4607  reuhypd  4617  ordsucim  4647  suc11g  4704  nlimsucg  4713  xpsspw  4887  funcnvuni  5450  fvmptdv2  5795  fsn  5880  fconst2g  5930  funfvima  5950  foco2  5959  isores3  6021  riotaeqimp  6063  eusvobj2  6071  ovmpodv2  6222  ovelrn  6238  f1opw2  6296  suppssov1  6299  suppssfvg  6503  nnmordi  6789  nnmord  6790  qsss  6868  eroveu  6900  th3qlem1  6911  mapsncnv  6977  elixpsn  7017  ixpsnf1o  7018  en1bg  7087  pw2f1odclem  7134  mapxpen  7148  mapunen  7151  en1eqsnbi  7266  updjud  7422  addnidpig  7703  enq0tr  7801  prcdnql  7851  prcunqu  7852  genipv  7876  genpelvl  7879  genpelvu  7880  distrlem5prl  7953  distrlem5pru  7954  aptiprlemu  8007  mulrid  8323  ltne  8410  cnegex  8504  creur  9290  creui  9291  cju  9292  nnsub  9344  un0addcl  9598  un0mulcl  9599  zaddcl  9686  elz2  9718  qmulz  10025  qre  10027  qnegcl  10038  elpqb  10052  xrltne  10217  xlesubadd  10287  iccid  10329  fzsn  10474  fzsuc2  10488  fz1sbc  10505  elfzp12  10508  modqmuladd  10805  bcval5  11203  bcpasc  11206  hashprg  11251  hashfzo  11265  wrdl1s1  11400  cats1un  11495  swrdccat3blem  11513  shftlem  11583  replim  11626  sqrtsq  11812  absle  11857  maxabslemval  11976  negfi  11996  xrmaxiflemval  12018  summodclem2  12151  summodc  12152  zsumdc  12153  fsum3  12156  fsummulc2  12217  fsum00  12231  isumsplit  12260  prodmodclem2  12346  prodmodc  12347  zproddc  12348  fprodseq  12352  prodsnf  12361  fzo0dvdseq  12626  divalgmod  12696  gcdabs1  12768  dvdsgcd  12791  dvdsmulgcd  12804  lcmgcdeq  12863  isprm2lem  12896  dvdsprime  12902  coprm  12924  prmdvdsexpr  12930  rpexp  12933  phibndlem  12996  dfphi2  13000  hashgcdlem  13018  odzdvds  13026  nnoddn2prm  13041  pythagtriplem1  13046  pceulem  13075  pcqmul  13084  pcqcl  13087  pcxnn0cl  13091  pcxcl  13092  pcneg  13106  pcabs  13107  pcgcd1  13109  pcz  13113  pcprmpw2  13114  pcprmpw  13115  dvdsprmpweqle  13118  difsqpwdvds  13119  pcaddlem  13120  pcadd  13121  pcmpt  13124  pockthg  13138  4sqlem2  13170  4sqlem4  13173  mul4sq  13175  ballotfilemfc0  13234  ballotfilemfcc  13235  mnd1id  13765  0subm  13793  mulgnn0p1  13938  mulgnn0ass  13963  dvreq1  14451  nzrunit  14497  rrgeq0  14575  domneq0  14583  lmodfopnelem2  14664  lss1d  14722  lspsneq0  14765  gsumfsum  14925  znidom  14994  znunit  14996  znrrg  14997  istopon  15116  eltg3  15160  tgidm  15177  restbasg  15271  tgrest  15272  tgcn  15311  cnconst  15337  lmss  15349  txbas  15361  txbasval  15370  upxp  15375  blssps  15530  blss  15531  metrest  15609  blssioo  15656  elcncf1di  15682  elply2  15838  plyf  15840  dvdsppwf1o  16109  perfectlem2  16120  perfect  16121  lgsmod  16157  lgsne0  16169  lgsdirnn0  16178  gausslemma2dlem1a  16189  gausslemma2dlem6  16198  lgseisenlem2  16202  lgsquadlem1  16208  lgsquadlem2  16209  2lgslem1b  16220  2sqlem2  16246  mul2sq  16247  2sqlem7  16252  lpvtx  16332  usgredgop  16426  uhgrspansubgrlem  16529  vtxd0nedgbfi  16552  wlk1walkdom  16612  upgrwlkvtxedg  16617  clwwlkext2edg  16675  clwwlknonccat  16686  bj-peano4  16993