Theorem syl5ibrcom 250

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  biimprcd  253  iftrueb  4502  elsn2g  4632  preq1b  4812  elpreqprb  4834  reusv3  5374  alxfr  5376  reuhypd  5388  axpr  5396  opth1  5455  euotd  5494  otiunsndisj  5501  tz7.2  5642  frsn  5747  dmopab2rex  5905  elsnxp  6290  reuop  6292  dfpo2  6295  ordtri1  6392  ordtri3  6395  fvmptdv2  7006  fveqressseq  7072  foco2  7102  fsn  7129  fnsnbg  7160  fnsnbOLD  7162  fmptsng  7164  fmptsnd  7165  fconst2g  7199  fnprb  7204  fntpb  7205  funfvima  7226  soisoi  7324  isores3  7331  eqfunresadj  7356  riotaeqimp  7391  eusvobj2  7400  ovmpodv2  7566  f1opw2  7663  sorpssun  7725  sorpssin  7726  oneqmin  7795  nlimsucg  7834  onzsl  7838  tfinds  7852  funcnvuni  7925  mptcnfimad  7979  opiota  8052  mposn  8094  mpof1o2d  8117  frpoins3xpg  8132  frpoins3xp3g  8133  poxp2  8135  xpord2pred  8137  sexp2  8138  poxp3  8142  xpord3pred  8144  sexp3  8145  xpord3inddlem  8146  suppssov1  8189  suppssov2  8190  suppssfv  8194  brtpos  8227  frrlem12  8290  frrlem13  8291  seqomlem1  8433  seqomlem2  8434  omordi  8547  omord  8549  omwordi  8552  oeeui  8584  nnmordi  8613  nnmord  8614  nnmwordi  8617  nnawordex  8619  nnaordex  8620  nneob  8638  omsmolem  8639  eldifsucnn  8646  qsss  8769  eroveu  8806  mapsncnv  8887  ralxpmap  8890  elixpsn  8931  ixpsnf1o  8932  boxcutc  8935  pw2f1olem  9065  2pwne  9117  mapxpen  9127  mapunen  9130  php  9187  onomeneq  9194  unxpdomlem2  9213  en1eqsnbi  9232  isfiniteg  9256  fofinf1o  9285  f1opwfi  9309  elfiun  9386  oieu  9497  brwdom2  9531  wdomtr  9533  ixpiunwdom  9548  en3lplem1  9577  suc11reg  9584  inf3lemd  9592  cantnfvalf  9630  cantnflt  9637  cantnfp1lem3  9645  cantnflem2  9655  ttrcltr  9681  rnttrcl  9687  ttrclselem1  9690  r1tr  9744  updjud  9916  dfac8alem  10009  wdomnumr  10044  isinfcard  10072  aceq3lem  10100  dfac5lem4  10106  dfac5  10108  dfac2b  10110  coftr  10253  fin23lem28  10320  fin23lem29  10321  fin1a2lem11  10390  fin1a2lem12  10391  fin1a2lem13  10392  hsmexlem9  10405  axdclem  10499  pwcfsdom  10564  gchdomtri  10610  fpwwe2  10624  gchpwdom  10651  gchhar  10660  addnidpi  10882  nqereu  10910  genpv  10980  genpdm  10983  distrlem5pr  11008  mulrid  11202  ltne  11303  mul02  11384  cnegex  11387  mul0or  11850  negfi  12160  sup2  12167  supaddc  12178  supadd  12179  supmul1  12180  supmul  12183  creur  12208  creui  12209  cju  12210  nnsub  12276  un0addcl  12533  un0mulcl  12534  nn0sub  12550  elz2  12605  zaddcl  12630  suprzcl2  12958  qmulz  12971  qre  12973  qnegcl  12986  elpqb  12996  xrmax1  13197  xrmin2  13200  max1ALT  13208  xlesubadd  13285  xmulass  13309  xlemul1a  13310  xrsupexmnf  13327  xrinfmexpnf  13328  xrub  13334  iccid  13413  fzsn  13590  fzsuc2  13606  fz1sbc  13624  elfzp12  13627  modmuladd  13945  seqid3  14078  bcval5  14350  bcpasc  14353  hashbnd  14368  hashnnn0genn0  14375  hashprg  14427  hashfzo  14462  tpfo  14533  wrdl1s1  14648  ccats1alpha  14653  cats1un  14754  s7f1o  14999  shftlem  15101  replim  15163  absmod0  15350  absz  15358  rlimdm  15598  summolem2  15763  summo  15764  zsum  15765  fsum  15767  fsummulc2  15831  fsumconst  15837  fsum00  15846  incexclem  15886  isumsplit  15890  infcvgaux1i  15907  prodmolem2  15985  prodmo  15986  zprod  15987  fprod  15991  prodsn  16012  prodsnf  16014  fprodconst  16028  ruclem2  16284  fzo0dvdseq  16377  bitsf1ocnv  16498  sadcaddlem  16511  smueqlem  16544  gcdabs1  16583  bezoutlem1  16593  bezoutlem3  16595  bezoutlem4  16596  dvdsgcd  16598  dvdsmulgcd  16610  lcmgcdeq  16666  lcmf  16687  lcmfunsnlem1  16691  lcmfunsnlem2lem2  16693  isprm2lem  16735  dvdsprime  16741  isprm5  16762  coprm  16766  prmdvdsexpr  16772  rpexp  16777  phibndlem  16825  dfphi2  16829  hashgcdlem  16843  odzdvds  16851  nnoddn2prm  16867  pythagtriplem1  16872  iserodd  16891  pceulem  16901  pcqmul  16909  pcqcl  16912  pcxnn0cl  16916  pcxcl  16917  pcneg  16930  pcabs  16931  pcgcd1  16933  pcz  16937  pcprmpw2  16938  pcprmpw  16939  dvdsprmpweqle  16942  difsqpwdvds  16943  pcaddlem  16944  pcadd  16945  pcmpt  16948  pockthg  16962  prmreclem5  16976  4sqlem4  17008  mul4sq  17010  vdwapun  17030  vdwlem2  17038  vdwlem6  17042  vdwlem8  17044  vdwlem13  17049  0ram  17076  ram0  17078  ramcl  17085  cshwsiun  17155  wunress  17305  firest  17481  isssc  17873  pospo  18395  latnlej  18508  gsumval2a  18739  xpsmnd0  18832  mnd1id  18834  0subm  18872  mulgnn0p1  19147  mulgnn0ass  19172  cyccom  19270  gicsubgen  19345  symg1bas  19457  snsymgefmndeq  19461  psgnunilem1  19559  psgnunilem2  19561  mndodcongi  19609  oddvdsnn0  19610  odnncl  19611  oddvds  19613  odeq  19616  odeq1  19626  pgpfi2  19672  sylow2a  19685  sylow2blem3  19688  sylow3lem6  19698  lsmelvalm  19717  lsmsubm  19719  lsmsubg  19720  lsmmod  19741  lsmdisj2  19748  efgmnvl  19780  efgtlen  19792  efgs1b  19802  efgrelexlemb  19816  efgredeu  19818  efgcpbllemb  19821  frgpuptinv  19837  frgpup3lem  19843  qusabl  19931  frgpnabllem1  19939  cyggeninv  19949  cyggenod  19950  gsumval3eu  19970  dprdssv  20084  dprdfeq0  20090  dprdsubg  20092  dprddisj2  20107  ablfacrp  20134  pgpfac1lem3  20145  pgpfaclem2  20150  xpsring1d  20411  dvreq1  20489  irredn1  20504  nzrunit  20604  ringcinv  20752  rrgeq0  20781  domneq0  20789  isabvd  20889  abvdom  20907  issrngd  20932  lmodfopnelem2  20994  lss1d  21058  lspsneq0  21107  lbspss  21177  lsmcl  21178  lvecvs0or  21206  lspindpi  21230  lidl1el  21325  lpiss  21462  lidldvgen  21467  qsssubdrg  21541  zringlpirlem1  21577  pzriprnglem6  21601  pzriprnglem12  21607  znfld  21675  znunit  21678  znrrg  21680  cygznlem3  21684  frgpcyg  21688  psgnghm  21695  ipeq0  21753  cssincl  21803  lsmcss  21807  obselocv  21843  dsmmacl  21856  dsmmlss  21859  mplsubrglem  22118  mplmonmul  22152  mplcoe5lem  22155  mhpsclcl  22275  mhpvarcl  22276  psdmul  22294  coe1tmmul2  22402  coe1tmmul  22403  pf1ind  22480  mat1dimelbas  22593  mdetralt  22730  mdetunilem2  22735  mdetunilem7  22740  mdetunilem9  22742  maducoeval2  22762  chpscmat  22964  chfacfscmulgsum  22982  chfacfpmmulgsum  22986  istopon  23034  eltg3  23084  tgidm  23102  clsval2  23172  opncldf1  23206  restbas  23280  tgrest  23281  restcld  23294  restcldr  23296  restcls  23303  restntr  23304  ordtbas2  23313  ordtbas  23314  ordtrest2lem  23325  ordtrest2  23326  pnfnei  23342  mnfnei  23343  tgcn  23374  cnconst  23406  cnindis  23414  lmss  23420  ordtt1  23501  discmp  23520  1stcrest  23575  2ndcdisj  23578  cldllycmp  23617  txbas  23689  ptpjpre1  23693  ptuni2  23698  ptbasin  23699  ptbasfi  23703  ptopn2  23706  txbasval  23728  ptpjopn  23734  ptclsg  23737  dfac14lem  23739  xkoccn  23741  ptcnp  23744  upxp  23745  ptrescn  23761  txkgen  23774  xkoptsub  23776  xkopt  23777  xkoco1cn  23779  xkoco2cn  23780  xkococn  23782  xkoinjcn  23809  ordthmeolem  23923  ptuncnv  23929  nrmhaus  23948  fbssint  23960  fbfinnfr  23963  fbasrn  24006  isufil2  24030  filufint  24042  rnelfm  24075  fmfnfmlem2  24077  fmfnfmlem3  24078  fmfnfmlem4  24079  fmfnfm  24080  flimtopon  24092  flimclslem  24106  fclstopon  24134  fclscf  24147  flimfnfcls  24150  alexsublem  24166  alexsubALTlem3  24171  alexsubALTlem4  24172  ptcmplem2  24175  tmdgsum2  24218  symgtgp  24228  cldsubg  24233  qustgplem  24243  tgptsmscld  24273  tsmsxplem1  24275  imasdsf1olem  24495  blssps  24546  blss  24547  stdbdxmet  24637  methaus  24642  metrest  24646  nrginvrcn  24814  nmoeq0  24858  blssioo  24917  xrtgioo  24929  xrsxmet  24932  reconnlem1  24949  reconnlem2  24950  xrge0tsms  24957  elcncf1di  25019  iccpnfcnv  25068  evth  25083  lebnumlem1  25085  lebnumlem2  25086  lebnumlem3  25087  nmoleub3  25243  minveclem3b  25552  ivthlem2  25576  ivthlem3  25577  elovolm  25599  ovolmge0  25601  ovoliun  25629  ovolicc2lem3  25643  ovolicc2  25646  voliunlem3  25676  dyaddisj  25720  dyadmax  25722  opnmblALT  25727  ismbfd  25763  ismbf2d  25764  mbfimaopnlem  25779  mbfimaopn2  25781  i1fmullem  25818  i1fres  25829  itg1climres  25838  mbfi1fseqlem4  25842  itg2lcl  25851  itgsplitioo  25962  ellimc2  26001  rolle  26114  dvlip  26117  dvge0  26130  dvne0  26135  lhop1lem  26137  tdeglem4  26182  degltlem1  26194  deg1nn0clb  26212  deg1lt0  26213  dvdsq1p  26285  ply1rem  26288  fta1g  26292  elply2  26318  plyf  26320  ne0p  26329  plyeq0lem  26332  plypf1  26334  0dgrb  26368  coe1termlem  26380  dgrcolem2  26396  plymul0or  26404  plyrem  26431  fta1  26434  quotcan  26435  aalioulem3  26460  eff1olem  26675  lognegb  26717  eflogeq  26729  argregt0  26737  argrege0  26738  tanarg  26746  cxpexp  26795  cxpeq0  26805  mulcxp  26812  cxpeq  26884  atans2  27058  scvxcvx  27112  dmgmaddn0  27149  isppw2  27241  vmappw  27242  vmacl  27244  efvmacl  27246  isnsqf  27261  mumullem2  27306  sqff1o  27308  dvdsppwf1o  27312  ppiublem1  27328  vmalelog  27331  chtublem  27337  fsumvma  27339  perfectlem2  27356  perfect  27357  bposlem1  27410  lgsmod  27449  lgsne0  27461  lgsdirnn0  27470  lgsqr  27477  lgsdchr  27481  gausslemma2dlem1a  27491  gausslemma2dlem6  27498  lgseisenlem2  27502  lgsquadlem1  27506  lgsquadlem2  27507  2lgslem1b  27518  2sqlem2  27544  mul2sq  27545  2sqlem7  27550  dchrisum0fno1  27637  pntrsumbnd2  27693  ostthlem1  27753  ostth2lem2  27760  ostth3  27764  ostth  27765  nolesgn2ores  27798  nogesgn1ores  27800  nolt02o  27821  nogt01o  27822  nosupbnd2  27842  noinfbnd2lem1  27856  noetasuplem4  27862  noetainflem4  27866  maxs1  27895  mins2  27898  ltsne  27900  eqcuts3  27959  cuteq1  27972  madef  27991  ltslpss  28063  lrrecfr  28098  addsval  28117  addsproplem2  28125  addsuniflem  28156  addbdaylem  28172  negsid  28196  negsunif  28210  mulsproplem5  28275  mulsproplem6  28276  mulsproplem7  28277  mulsproplem8  28278  mulsproplem9  28279  lemulsd  28293  sltmuls1  28302  sltmuls2  28303  ltmuls2  28326  muls0ord  28340  precsexlem8  28369  precsexlem9  28370  precsexlem11  28372  elons2  28413  oncutlt  28419  bdayons  28431  onaddscl  28432  onmulscl  28433  nnsge1  28498  n0fincut  28510  n0subs  28518  dfnns2  28527  eucliddivs  28531  znegscl  28547  zaddscl  28549  zmulscld  28552  elzn0s  28553  eln0zs  28555  n0seo  28576  zseo  28577  bdaypw2n0bndlem  28618  bdaypw2n0bnd  28619  z12no  28631  z12addscl  28632  z12negscl  28633  z12shalf  28635  z12zsodd  28637  z12sge0  28638  z12bdaylem  28639  bdayfinlem  28641  recut  28649  elreno2  28650  remulscllem1  28655  colinearalg  29197  axpasch  29228  axlowdimlem16  29244  axlowdimlem17  29245  axlowdim  29248  axcontlem2  29252  axcontlem4  29254  axcontlem7  29257  lpvtx  29355  edglnl  29430  numedglnl  29431  usgredgop  29457  usgrexmplef  29546  uhgrspansubgrlem  29577  uhgrspan1  29590  nbusgredgeu0  29655  nb3grprlem2  29668  cusgrsize2inds  29740  vtxd0nedgb  29775  rusgrpropnb  29870  upgrwlkvtxedg  29931  wlkp1lem1  29958  wlkp1lem6  29963  wlkp1lem8  29965  usgr2wlkneq  30042  crctcshwlk  30108  crctcsh  30110  iswwlksnon  30139  wlkiswwlks1  30153  wwlksnextbi  30180  wwlksnextproplem2  30196  wspthsnonn0vne  30203  clwlkclwwlklem2  30288  clwwisshclwws  30303  erclwwlktr  30310  clwwlkel  30334  clwwlkext2edg  30344  erclwwlkntr  30359  clwlknf1oclwwlknlem2  30370  clwlknf1oclwwlknlem3  30371  clwlknf1oclwwlkn  30372  clwwlknonccat  30384  0wlkons1  30409  3wlkdlem6  30453  eupth2eucrct  30505  frgrwopreglem2  30601  2clwwlk2clwwlk  30638  wlkl0  30655  nvmul0or  30939  ipasslem5  31124  ipasslem11  31129  hvmul0or  31314  his6  31388  hhssnv  31553  ocsh  31572  ocin  31585  shsidmi  31673  chnlen0  31733  h1de2bi  31843  h1de2ctlem  31844  h1de2ci  31845  spansni  31846  3oalem1  31951  nmcexi  32315  atcveq0  32637  chcv1  32644  cdjreui  32721  cdj3lem2b  32726  xrge0tsmsd  33330  1fldgenq  33582  psrmonmul  33881  ccfldextdgrr  34003  ordtrest2NEWlem  34253  ordtrest2NEW  34254  xrge0iifcnv  34264  esumc  34382  esumpcvgval  34409  ballotlemfc0  34824  ballotlemfcc  34825  fissorduni  35419  axprALT2  35441  fineqvnttrclse  35456  gblacfnacd  35481  vonf1oonfo  35494  onvfowev  35495  subfacp1lem4  35570  subfacp1lem5  35571  erdszelem8  35585  sconnpi1  35626  cvmsss2  35661  cvmlift2lem12  35701  satfv0  35745  satfv0fun  35758  satf00  35761  sat1el2xp  35766  fmla0xp  35770  fmlasucdisj  35786  satffunlem1lem1  35789  satffunlem2lem1  35791  dmopab3rexdif  35792  msubco  35918  msubvrs  35947  ellcsrspsn  36028  sinccvglem  36059  untsucf  36097  nnuni  36114  dfrdg2  36180  colineardim1  36448  btwnconn1lem14  36487  segleantisym  36502  colinbtwnle  36505  outsidele  36519  lineunray  36534  linethru  36540  nmulprop  36577  elicc3  36713  opnregcld  36726  cldregopn  36727  fnejoin2  36765  bj-isrvec  37821  dissneqlem  37869  icorempo  37880  relowlssretop  37892  relowlpssretop  37893  rdgssun  37907  finxpsuclem  37926  lindsenlbs  38149  ptrecube  38154  poimirlem6  38160  poimirlem7  38161  poimirlem16  38170  poimirlem17  38171  poimirlem19  38173  poimirlem20  38174  poimirlem21  38175  poimirlem22  38176  poimirlem23  38177  poimirlem24  38178  poimirlem25  38179  poimirlem26  38180  poimirlem27  38181  poimirlem29  38183  poimirlem30  38184  poimirlem31  38185  poimirlem32  38186  itg2addnclem3  38207  ftc1anclem6  38232  dvasin  38238  unirep  38248  sdclem2  38276  ssbnd  38322  prdsbnd  38327  cntotbnd  38330  heibor1lem  38343  rrnequiv  38369  ismndo2  38408  grpoeqdivid  38415  isdrngo3  38493  crngohomfo  38540  0idl  38559  1idl  38560  divrngidl  38562  smprngopr  38586  prnc  38601  ispridlc  38604  disjimeceqim  39338  riotaclbgBAD  39613  lshpdisj  39646  lsateln0  39654  lsatcveq0  39691  opnlen0  39847  cmtbr4N  39914  cvrnbtwn2  39934  cvrnbtwn4  39938  atcvreq0  39973  cvlatexch1  39995  exatleN  40063  atlelt  40097  ps-2  40137  llnn0  40175  lplnn0N  40206  islpln2a  40207  lvoln0N  40250  islvol2aN  40251  4at  40272  dalemcea  40319  dalem3  40323  pmapglb2N  40430  pmapglb2xN  40431  cdlema1N  40450  cdlemb  40453  paddasslem17  40495  llnexchb2lem  40527  llnexchb2  40528  lhpat3  40705  ltrnid  40794  trlne  40844  cdlemc4  40853  cdleme11h  40925  cdlemednuN  40959  cdlemg1a  41229  tendoeq2  41433  tendoid0  41484  dva1dim  41644  dib1dim  41824  dihlatat  41996  dochkrshp4  42048  dochkr1  42137  lclkrlem2e  42170  lcfrlem16  42217  lcfrlem28  42229  mapd0  42324  hdmap14lem13  42539  eqresfnbd  42888  expeq1d  42970  expeqidd  42971  dvdsexpnn0  42980  reladdrsub  43031  sn-remul0ord  43054  sn-negex12  43063  sn-mullid  43082  sn-mul02  43111  nn0addcom  43121  nn0mulcom  43125  zmulcomlem  43126  mulgt0con1d  43129  mulgt0con2d  43130  sn-sup2  43150  frlmsnic  43195  evlselvlem  43207  prjspner1  43245  elrfi  43312  mrefg2  43325  eldiophb  43375  eldioph2b  43381  diophin  43390  diophun  43391  rexzrexnn0  43418  eldioph4b  43425  diophren  43427  rencldnfilem  43434  pellexlem6  43448  jm2.19  43607  rmydioph  43628  expdiophlem1  43635  expdioph  43637  lnr2i  43730  lpirlnr  43731  hbtlem2  43738  hbtlem4  43740  hbtlem6  43743  dgrsub2  43749  dgraa0p  43763  rngunsnply  43783  nlimsuc  44054  dfsucon  44136  radcnvrat  44911  pm14.24  45029  addrcom  45070  modelaxreplem1  45574  ormklocald  47477  natlocalincr  47479  afveu  47774  dfafn5b  47782  rlimdmafv  47798  afv2eu  47859  rlimdmafv2  47879  el1fzopredsuc  47947  minusmod5ne  47976  modmknepk  47989  elsetpreimafvssdm  48019  imasetpreimafvbijlemfo  48038  sprvalpw  48113  prprvalpw  48148  reupr  48155  fmtnofac2lem  48204  proththdlem  48249  perfectALTVlem2  48371  perfectALTV  48372  gbowpos  48408  gbowgt5  48411  gboge9  48413  nnsum4primesodd  48445  nnsum4primesoddALTV  48446  uhgrimedgi  48539  isuspgrim0  48543  isuspgrimlem  48544  upgrimpths  48558  clnbgrgrim  48583  grimedg  48584  grtrissvtx  48593  stgredgiun  48607  stgrvtx0  48611  isubgr3stgrlem7  48621  grlimgrtrilem2  48651  gpgiedgdmellem  48695  gpgvtxel2  48697  gpgvtx0  48702  gpgvtx1  48703  gpgusgralem  48705  gpgedgvtx0  48710  gpgedgvtx1  48711  gpgedg2ov  48715  gpgedg2iv  48716  gpgnbgrvtx0  48723  gpgnbgrvtx1  48724  pgnbgreunbgr  48774  ringcinvALTV  48959  smprngprmrng  48988  lincellss  49086  lindsrng01  49128  suppdm  49170  nnpw2pb  49247  0aryfvalel  49294  0aryfvalelfv  49295  itsclc0xyqsolr  49429  infsubc  49718  infsubc2  49719