Theorem syl5ibrcom 246

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 245	. 2 ⊢ (𝜒 → (𝜑 → 𝜓))
4	3	com12 32	1 ⊢ (𝜑 → (𝜒 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  biimprcd  249  elsn2g  4665  preq1b  4846  elpreqprb  4867  reusv3  5402  alxfr  5404  reuhypd  5416  opth1  5474  euotd  5512  otiunsndisj  5519  tz7.2  5659  frsn  5762  dmopab2rex  5916  elsnxp  6289  reuop  6291  dfpo2  6294  ordtri1  6396  ordtri3  6399  fvmptdv2  7015  fveqressseq  7080  foco2  7109  fsn  7134  fnsnb  7165  fmptsng  7167  fmptsnd  7168  fconst2g  7205  fnprb  7211  fntpb  7212  funfvima  7233  soisoi  7327  isores3  7334  eqfunresadj  7359  riotaeqimp  7394  eusvobj2  7403  ovmpodv2  7568  f1opw2  7663  sorpssun  7722  sorpssin  7723  oneqmin  7790  nlimsucg  7833  onzsl  7837  tfinds  7851  funcnvuni  7924  opiota  8047  mposn  8091  frpoins3xpg  8128  frpoins3xp3g  8129  poxp2  8131  xpord2pred  8133  sexp2  8134  poxp3  8138  xpord3pred  8140  sexp3  8141  xpord3inddlem  8142  suppssov1  8185  suppssfv  8189  brtpos  8222  frrlem12  8284  frrlem13  8285  wfrlem10OLD  8320  wfrlem14OLD  8324  wfrlem15OLD  8325  seqomlem1  8452  seqomlem2  8453  omordi  8568  omord  8570  omwordi  8573  oeeui  8604  nnmordi  8633  nnmord  8634  nnmwordi  8637  nnawordex  8639  nnaordex  8640  nneob  8657  omsmolem  8658  eldifsucnn  8665  qsss  8774  eroveu  8808  mapsncnv  8889  ralxpmap  8892  elixpsn  8933  ixpsnf1o  8934  boxcutc  8937  pw2f1olem  9078  2pwne  9135  mapxpen  9145  mapunen  9148  php  9212  phpOLD  9224  onomeneq  9230  unxpdomlem2  9253  en1eqsnbi  9278  isfiniteg  9306  fofinf1o  9329  f1opwfi  9358  elfiun  9427  oieu  9536  brwdom2  9570  wdomtr  9572  ixpiunwdom  9587  en3lplem1  9609  suc11reg  9616  inf3lemd  9624  cantnfvalf  9662  cantnflt  9669  cantnfp1lem3  9677  cantnflem2  9687  ttrcltr  9713  rnttrcl  9719  ttrclselem1  9722  r1tr  9773  updjud  9931  dfac8alem  10026  wdomnumr  10061  isinfcard  10089  aceq3lem  10117  dfac5lem4  10123  dfac5  10125  dfac2b  10127  coftr  10270  fin23lem28  10337  fin23lem29  10338  fin1a2lem11  10407  fin1a2lem12  10408  fin1a2lem13  10409  hsmexlem9  10422  axdclem  10516  pwcfsdom  10580  gchdomtri  10626  fpwwe2  10640  gchpwdom  10667  gchhar  10676  addnidpi  10898  nqereu  10926  genpv  10996  genpdm  10999  distrlem5pr  11024  mulrid  11216  ltne  11315  mul02  11396  cnegex  11399  mul0or  11858  negfi  12167  sup2  12174  supaddc  12185  supadd  12186  supmul1  12187  supmul  12190  creur  12210  creui  12211  cju  12212  nnsub  12260  un0addcl  12509  un0mulcl  12510  nn0sub  12526  elz2  12580  zaddcl  12606  suprzcl2  12926  qmulz  12939  qre  12941  qnegcl  12954  elpqb  12964  xrmax1  13158  xrmin2  13161  max1ALT  13169  xlesubadd  13246  xmulass  13270  xlemul1a  13271  xrsupexmnf  13288  xrinfmexpnf  13289  xrub  13295  iccid  13373  fzsn  13547  fzsuc2  13563  fz1sbc  13581  elfzp12  13584  modmuladd  13882  seqid3  14016  bcval5  14282  bcpasc  14285  hashbnd  14300  hashnnn0genn0  14307  hashprg  14359  hashfzo  14393  wrdl1s1  14568  ccats1alpha  14573  cats1un  14675  shftlem  15019  replim  15067  absmod0  15254  absz  15262  rlimdm  15499  summolem2  15666  summo  15667  zsum  15668  fsum  15670  fsummulc2  15734  fsumconst  15740  fsum00  15748  incexclem  15786  isumsplit  15790  infcvgaux1i  15807  prodmolem2  15883  prodmo  15884  zprod  15885  fprod  15889  prodsn  15910  prodsnf  15912  fprodconst  15926  ruclem2  16179  fzo0dvdseq  16270  bitsf1ocnv  16389  sadcaddlem  16402  smueqlem  16435  gcdabs1  16474  bezoutlem1  16485  bezoutlem3  16487  bezoutlem4  16488  dvdsgcd  16490  dvdsmulgcd  16501  lcmgcdeq  16553  lcmf  16574  lcmfunsnlem1  16578  lcmfunsnlem2lem2  16580  isprm2lem  16622  dvdsprime  16628  isprm5  16648  coprm  16652  prmdvdsexpr  16658  rpexp  16663  phibndlem  16707  dfphi2  16711  hashgcdlem  16725  odzdvds  16732  nnoddn2prm  16748  pythagtriplem1  16753  iserodd  16772  pceulem  16782  pcqmul  16790  pcqcl  16793  pcxnn0cl  16797  pcxcl  16798  pcneg  16811  pcabs  16812  pcgcd1  16814  pcz  16818  pcprmpw2  16819  pcprmpw  16820  dvdsprmpweqle  16823  difsqpwdvds  16824  pcaddlem  16825  pcadd  16826  pcmpt  16829  pockthg  16843  prmreclem5  16857  4sqlem4  16889  mul4sq  16891  vdwapun  16911  vdwlem2  16919  vdwlem6  16923  vdwlem8  16925  vdwlem13  16930  0ram  16957  ram0  16959  ramcl  16966  cshwsiun  17037  wunress  17199  wunressOLD  17200  firest  17382  isssc  17771  pospo  18302  latnlej  18413  gsumval2a  18610  xpsmnd0  18700  mnd1id  18702  0subm  18734  mulgnn0p1  19001  mulgnn0ass  19026  cyccom  19118  gicsubgen  19193  symg1bas  19299  snsymgefmndeq  19303  psgnunilem1  19402  psgnunilem2  19404  mndodcongi  19452  oddvdsnn0  19453  odnncl  19454  oddvds  19456  odeq  19459  odeq1  19469  pgpfi2  19515  sylow2a  19528  sylow2blem3  19531  sylow3lem6  19541  lsmelvalm  19560  lsmsubm  19562  lsmsubg  19563  lsmmod  19584  lsmdisj2  19591  efgmnvl  19623  efgtlen  19635  efgs1b  19645  efgrelexlemb  19659  efgredeu  19661  efgcpbllemb  19664  frgpuptinv  19680  frgpup3lem  19686  qusabl  19774  frgpnabllem1  19782  cyggeninv  19792  cyggenod  19793  gsumval3eu  19813  dprdssv  19927  dprdfeq0  19933  dprdsubg  19935  dprddisj2  19950  ablfacrp  19977  pgpfac1lem3  19988  pgpfaclem2  19993  xpsring1d  20221  dvreq1  20302  irredn1  20317  nzrunit  20413  drngmul0or  20529  isabvd  20571  abvdom  20589  issrngd  20612  lmodfopnelem2  20653  lss1d  20718  lspsneq0  20767  lbspss  20837  lsmcl  20838  lvecvs0or  20866  lspindpi  20890  lidl1el  20990  lpiss  21088  lidldvgen  21093  rrgeq0  21106  domneq0  21113  qsssubdrg  21204  zringlpirlem1  21233  pzriprnglem6  21255  pzriprnglem12  21261  znfld  21335  znunit  21338  znrrg  21340  cygznlem3  21344  frgpcyg  21348  psgnghm  21352  ipeq0  21410  cssincl  21460  lsmcss  21464  obselocv  21502  dsmmacl  21515  dsmmlss  21518  mplsubrglem  21782  mplmonmul  21810  mplcoe5lem  21813  mhpsclcl  21909  mhpvarcl  21910  coe1tmmul2  22018  coe1tmmul  22019  pf1ind  22094  mat1dimelbas  22193  mdetralt  22330  mdetunilem2  22335  mdetunilem7  22340  mdetunilem9  22342  maducoeval2  22362  chpscmat  22564  chfacfscmulgsum  22582  chfacfpmmulgsum  22586  istopon  22634  eltg3  22685  tgidm  22703  clsval2  22774  opncldf1  22808  restbas  22882  tgrest  22883  restcld  22896  restcldr  22898  restcls  22905  restntr  22906  ordtbas2  22915  ordtbas  22916  ordtrest2lem  22927  ordtrest2  22928  pnfnei  22944  mnfnei  22945  tgcn  22976  cnconst  23008  cnindis  23016  lmss  23022  ordtt1  23103  discmp  23122  1stcrest  23177  2ndcdisj  23180  cldllycmp  23219  txbas  23291  ptpjpre1  23295  ptuni2  23300  ptbasin  23301  ptbasfi  23305  ptopn2  23308  txbasval  23330  ptpjopn  23336  ptclsg  23339  dfac14lem  23341  xkoccn  23343  ptcnp  23346  upxp  23347  ptrescn  23363  txkgen  23376  xkoptsub  23378  xkopt  23379  xkoco1cn  23381  xkoco2cn  23382  xkococn  23384  xkoinjcn  23411  ordthmeolem  23525  ptuncnv  23531  nrmhaus  23550  fbssint  23562  fbfinnfr  23565  fbasrn  23608  isufil2  23632  filufint  23644  rnelfm  23677  fmfnfmlem2  23679  fmfnfmlem3  23680  fmfnfmlem4  23681  fmfnfm  23682  flimtopon  23694  flimclslem  23708  fclstopon  23736  fclscf  23749  flimfnfcls  23752  alexsublem  23768  alexsubALTlem3  23773  alexsubALTlem4  23774  ptcmplem2  23777  tmdgsum2  23820  symgtgp  23830  cldsubg  23835  qustgplem  23845  tgptsmscld  23875  tsmsxplem1  23877  imasdsf1olem  24099  blssps  24150  blss  24151  stdbdxmet  24244  methaus  24249  metrest  24253  nrginvrcn  24429  nmoeq0  24473  blssioo  24531  xrtgioo  24542  xrsxmet  24545  reconnlem1  24562  reconnlem2  24563  xrge0tsms  24570  elcncf1di  24635  iccpnfcnv  24689  evth  24705  lebnumlem1  24707  lebnumlem2  24708  lebnumlem3  24709  nmoleub3  24866  minveclem3b  25176  ivthlem2  25201  ivthlem3  25202  elovolm  25224  ovolmge0  25226  ovoliun  25254  ovolicc2lem3  25268  ovolicc2  25271  voliunlem3  25301  dyaddisj  25345  dyadmax  25347  opnmblALT  25352  ismbfd  25388  ismbf2d  25389  mbfimaopnlem  25404  mbfimaopn2  25406  i1fmullem  25443  i1fres  25455  itg1climres  25464  mbfi1fseqlem4  25468  itg2lcl  25477  itgsplitioo  25587  ellimc2  25626  rolle  25742  dvlip  25745  dvge0  25758  dvne0  25763  lhop1lem  25765  tdeglem4  25812  tdeglem4OLD  25813  degltlem1  25825  deg1nn0clb  25843  deg1lt0  25844  dvdsq1p  25913  ply1rem  25916  fta1g  25920  elply2  25945  plyf  25947  ne0p  25956  plyeq0lem  25959  plypf1  25961  0dgrb  25995  coe1termlem  26007  dgrcolem2  26024  plymul0or  26030  plyrem  26054  fta1  26057  quotcan  26058  aalioulem3  26083  eff1olem  26293  lognegb  26334  eflogeq  26346  argregt0  26354  argrege0  26355  tanarg  26363  cxpexp  26412  cxpeq0  26422  mulcxp  26429  cxpeq  26501  atans2  26672  scvxcvx  26726  dmgmaddn0  26763  isppw2  26855  vmappw  26856  vmacl  26858  efvmacl  26860  isnsqf  26875  mumullem2  26920  sqff1o  26922  dvdsppwf1o  26926  ppiublem1  26941  vmalelog  26944  chtublem  26950  fsumvma  26952  perfectlem2  26969  perfect  26970  bposlem1  27023  lgsmod  27062  lgsne0  27074  lgsdirnn0  27083  lgsqr  27090  lgsdchr  27094  gausslemma2dlem1a  27104  gausslemma2dlem6  27111  lgseisenlem2  27115  lgsquadlem1  27119  lgsquadlem2  27120  2lgslem1b  27131  2sqlem2  27157  mul2sq  27158  2sqlem7  27163  dchrisum0fno1  27250  pntrsumbnd2  27306  ostthlem1  27366  ostth2lem2  27373  ostth3  27377  ostth  27378  nolesgn2ores  27411  nogesgn1ores  27413  nolt02o  27434  nogt01o  27435  nosupbnd2  27455  noinfbnd2lem1  27469  noetasuplem4  27475  noetainflem4  27479  maxs1  27504  mins2  27507  sltne  27509  ssltsn  27530  cuteq1  27571  madef  27588  sltlpss  27638  lrrecfr  27665  addsval  27684  addsproplem2  27692  addsuniflem  27723  negsid  27754  negsunif  27768  mulsproplem5  27815  mulsproplem6  27816  mulsproplem7  27817  mulsproplem8  27818  mulsproplem9  27819  slemuld  27833  ssltmul1  27841  ssltmul2  27842  sltmul2  27862  precsexlem8  27899  precsexlem9  27900  precsexlem11  27902  elons2  27924  colinearalg  28435  axpasch  28466  axlowdimlem16  28482  axlowdimlem17  28483  axlowdim  28486  axcontlem2  28490  axcontlem4  28492  axcontlem7  28495  lpvtx  28595  edglnl  28670  numedglnl  28671  usgredgop  28697  usgrexmplef  28783  uhgrspansubgrlem  28814  uhgrspan1  28827  nbusgredgeu0  28892  nb3grprlem2  28905  cusgrsize2inds  28977  vtxd0nedgb  29012  rusgrpropnb  29107  upgrwlkvtxedg  29169  wlkp1lem1  29197  wlkp1lem6  29202  wlkp1lem8  29204  usgr2wlkneq  29280  crctcshwlk  29343  crctcsh  29345  iswwlksnon  29374  wlkiswwlks1  29388  wwlksnextbi  29415  wwlksnextproplem2  29431  wspthsnonn0vne  29438  clwlkclwwlklem2  29520  clwwisshclwws  29535  erclwwlktr  29542  clwwlkel  29566  clwwlkext2edg  29576  erclwwlkntr  29591  clwlknf1oclwwlknlem2  29602  clwlknf1oclwwlknlem3  29603  clwlknf1oclwwlkn  29604  clwwlknonccat  29616  0wlkons1  29641  3wlkdlem6  29685  eupth2eucrct  29737  frgrwopreglem2  29833  2clwwlk2clwwlk  29870  wlkl0  29887  nvmul0or  30170  ipasslem5  30355  ipasslem11  30360  hvmul0or  30545  his6  30619  hhssnv  30784  ocsh  30803  ocin  30816  shsidmi  30904  chnlen0  30964  h1de2bi  31074  h1de2ctlem  31075  h1de2ci  31076  spansni  31077  3oalem1  31182  nmcexi  31546  atcveq0  31868  chcv1  31875  cdjreui  31952  cdj3lem2b  31957  xrge0tsmsd  32479  1fldgenq  32682  ccfldextdgrr  33035  ordtrest2NEWlem  33200  ordtrest2NEW  33201  xrge0iifcnv  33211  esumc  33347  esumpcvgval  33374  ballotlemfc0  33789  ballotlemfcc  33790  subfacp1lem4  34472  subfacp1lem5  34473  erdszelem8  34487  sconnpi1  34528  cvmsss2  34563  cvmlift2lem12  34603  satfv0  34647  satfv0fun  34660  satf00  34663  sat1el2xp  34668  fmla0xp  34672  fmlasucdisj  34688  satffunlem1lem1  34691  satffunlem2lem1  34693  dmopab3rexdif  34694  msubco  34820  msubvrs  34849  sinccvglem  34955  untsucf  34983  nnuni  35000  dfrdg2  35071  colineardim1  35337  btwnconn1lem14  35376  segleantisym  35391  colinbtwnle  35394  outsidele  35408  lineunray  35423  linethru  35429  elicc3  35505  opnregcld  35518  cldregopn  35519  fnejoin2  35557  bj-isrvec  36478  dissneqlem  36524  icorempo  36535  relowlssretop  36547  relowlpssretop  36548  rdgssun  36562  finxpsuclem  36581  lindsenlbs  36786  ptrecube  36791  poimirlem6  36797  poimirlem7  36798  poimirlem16  36807  poimirlem17  36808  poimirlem19  36810  poimirlem20  36811  poimirlem21  36812  poimirlem22  36813  poimirlem23  36814  poimirlem24  36815  poimirlem25  36816  poimirlem26  36817  poimirlem27  36818  poimirlem29  36820  poimirlem30  36821  poimirlem31  36822  poimirlem32  36823  itg2addnclem3  36844  ftc1anclem6  36869  dvasin  36875  unirep  36885  sdclem2  36913  ssbnd  36959  prdsbnd  36964  cntotbnd  36967  heibor1lem  36980  rrnequiv  37006  ismndo2  37045  grpoeqdivid  37052  isdrngo3  37130  crngohomfo  37177  0idl  37196  1idl  37197  divrngidl  37199  smprngopr  37223  prnc  37238  ispridlc  37241  riotaclbgBAD  38127  lshpdisj  38160  lsateln0  38168  lsatcveq0  38205  opnlen0  38361  cmtbr4N  38428  cvrnbtwn2  38448  cvrnbtwn4  38452  atcvreq0  38487  cvlatexch1  38509  exatleN  38578  atlelt  38612  ps-2  38652  llnn0  38690  lplnn0N  38721  islpln2a  38722  lvoln0N  38765  islvol2aN  38766  4at  38787  dalemcea  38834  dalem3  38838  pmapglb2N  38945  pmapglb2xN  38946  cdlema1N  38965  cdlemb  38968  paddasslem17  39010  llnexchb2lem  39042  llnexchb2  39043  lhpat3  39220  ltrnid  39309  trlne  39359  cdlemc4  39368  cdleme11h  39440  cdlemednuN  39474  cdlemg1a  39744  tendoeq2  39948  tendoid0  39999  dva1dim  40159  dib1dim  40339  dihlatat  40511  dochkrshp4  40563  dochkr1  40652  lclkrlem2e  40685  lcfrlem16  40732  lcfrlem28  40744  mapd0  40839  hdmap14lem13  41054  fnsnbt  41357  eqresfnbd  41360  f1o2d2  41361  frlmsnic  41412  evlselvlem  41460  dvdsexpnn0  41534  reladdrsub  41560  sn-negex12  41591  sn-mullid  41610  sn-mul02  41615  nn0addcom  41625  nn0mulcom  41629  zmulcomlem  41630  mulgt0con1d  41633  mulgt0con2d  41634  sn-sup2  41644  prjspner1  41670  elrfi  41734  mrefg2  41747  eldiophb  41797  eldioph2b  41803  diophin  41812  diophun  41813  rexzrexnn0  41844  eldioph4b  41851  diophren  41853  rencldnfilem  41860  pellexlem6  41874  jm2.19  42034  rmydioph  42055  expdiophlem1  42062  expdioph  42064  lnr2i  42160  lpirlnr  42161  hbtlem2  42168  hbtlem4  42170  hbtlem6  42173  dgrsub2  42179  dgraa0p  42193  rngunsnply  42217  nlimsuc  42494  dfsucon  42576  radcnvrat  43375  pm14.24  43493  addrcom  43536  natlocalincr  45888  afveu  46159  dfafn5b  46167  rlimdmafv  46183  afv2eu  46244  rlimdmafv2  46264  el1fzopredsuc  46331  elsetpreimafvssdm  46352  imasetpreimafvbijlemfo  46371  sprvalpw  46446  prprvalpw  46481  reupr  46488  fmtnofac2lem  46534  proththdlem  46579  perfectALTVlem2  46688  perfectALTV  46689  gbowpos  46725  gbowgt5  46728  gboge9  46730  nnsum4primesodd  46762  nnsum4primesoddALTV  46763  isomuspgr  46800  ringcinv  47018  ringcinvALTV  47042  lincellss  47194  lindsrng01  47236  suppdm  47278  nnpw2pb  47360  0aryfvalel  47407  0aryfvalelfv  47408  itsclc0xyqsolr  47542