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  4378  euotd  4397  tz7.2  4501  reusv3  4608  alxfr  4609  reuhypd  4619  ordsucim  4649  suc11g  4706  nlimsucg  4715  xpsspw  4889  funcnvuni  5453  fvmptdv2  5798  fsn  5883  fconst2g  5933  funfvima  5953  foco2  5962  isores3  6024  riotaeqimp  6066  eusvobj2  6074  ovmpodv2  6225  ovelrn  6241  f1opw2  6299  suppssov1  6302  suppssfvg  6507  nnmordi  6794  nnmord  6795  qsss  6873  eroveu  6905  th3qlem1  6916  mapsncnv  6983  elixpsn  7023  ixpsnf1o  7024  en1bg  7093  pw2f1odclem  7140  mapxpen  7154  mapunen  7157  en1eqsnbi  7273  updjud  7429  addnidpig  7710  enq0tr  7808  prcdnql  7858  prcunqu  7859  genipv  7883  genpelvl  7886  genpelvu  7887  distrlem5prl  7960  distrlem5pru  7961  aptiprlemu  8014  mulrid  8330  ltne  8417  cnegex  8512  creur  9298  creui  9299  cju  9300  nnsub  9353  un0addcl  9608  un0mulcl  9609  zaddcl  9694  elz2  9726  qmulz  10039  qre  10041  qnegcl  10052  elpqb  10067  xrltne  10232  xlesubadd  10302  iccid  10344  fzsn  10489  fzsuc2  10503  fz1sbc  10520  elfzp12  10523  modqmuladd  10824  bcval5  11223  bcpasc  11226  hashprg  11271  hashfzo  11285  wrdl1s1  11420  cats1un  11515  swrdccat3blem  11533  shftlem  11603  replim  11646  sqrtsq  11832  absle  11878  maxabslemval  11997  negfi  12017  xrmaxiflemval  12041  summodclem2  12174  summodc  12175  zsumdc  12176  fsum3  12179  fsummulc2  12240  fsum00  12254  isumsplit  12283  prodmodclem2  12369  prodmodc  12370  zproddc  12371  fprodseq  12375  prodsnf  12384  fzo0dvdseq  12649  divalgmod  12719  gcdabs1  12791  dvdsgcd  12814  dvdsmulgcd  12827  lcmgcdeq  12886  isprm2lem  12919  dvdsprime  12925  coprm  12948  prmdvdsexpr  12954  rpexp  12957  phibndlem  13023  dfphi2  13027  hashgcdlem  13045  odzdvds  13053  nnoddn2prm  13068  pythagtriplem1  13073  pceulem  13102  pcqmul  13111  pcqcl  13114  pcxnn0cl  13118  pcxcl  13119  pcneg  13133  pcabs  13134  pcgcd1  13136  pcz  13140  pcprmpw2  13141  pcprmpw  13142  dvdsprmpweqle  13145  difsqpwdvds  13146  pcaddlem  13147  pcadd  13148  pcmpt  13151  pockthg  13165  4sqlem2  13197  4sqlem4  13200  mul4sq  13202  prmlem1a  13250  ballotfilemfc0  13290  ballotfilemfcc  13291  mnd1id  13822  0subm  13850  mulgnn0p1  13995  mulgnn0ass  14020  dvreq1  14558  nzrunit  14604  rrgeq0  14682  domneq0  14690  lmodfopnelem2  14771  lss1d  14829  lspsneq0  14872  gsumfsum  15032  znidom  15101  znunit  15103  znrrg  15104  istopon  15272  eltg3  15316  tgidm  15333  restbasg  15427  tgrest  15428  tgcn  15467  cnconst  15493  lmss  15505  txbas  15517  txbasval  15526  upxp  15531  blssps  15686  blss  15687  metrest  15765  blssioo  15812  elcncf1di  15838  elply2  15994  plyf  15996  efnthr  16209  dvdsppwf1o  16316  ppiublem1  16324  chtublem  16328  perfectlem2  16333  perfect  16334  bposlem1  16344  lgsmod  16383  lgsne0  16395  lgsdirnn0  16404  gausslemma2dlem1a  16415  gausslemma2dlem6  16424  lgseisenlem2  16428  lgsquadlem1  16434  lgsquadlem2  16435  2lgslem1b  16446  2sqlem2  16472  mul2sq  16473  2sqlem7  16478  lpvtx  16558  usgredgop  16652  uhgrspansubgrlem  16755  vtxd0nedgbfi  16778  wlk1walkdom  16838  upgrwlkvtxedg  16843  clwwlkext2edg  16901  clwwlknonccat  16912  bj-peano4  17219