Theorem syl5ibrcom 247

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  biimprcd  250  iftrueb  4492  elsn2g  4621  preq1b  4802  elpreqprb  4824  reusv3  5350  alxfr  5352  reuhypd  5364  axpr  5372  opth1  5423  euotd  5461  otiunsndisj  5468  tz7.2  5607  frsn  5712  dmopab2rex  5866  elsnxp  6249  reuop  6251  dfpo2  6254  ordtri1  6350  ordtri3  6353  fvmptdv2  6959  fveqressseq  7024  foco2  7054  fsn  7080  fnsnbg  7110  fnsnbOLD  7112  fmptsng  7114  fmptsnd  7115  fconst2g  7149  fnprb  7154  fntpb  7155  funfvima  7176  soisoi  7274  isores3  7281  eqfunresadj  7306  riotaeqimp  7341  eusvobj2  7350  ovmpodv2  7516  f1opw2  7613  sorpssun  7675  sorpssin  7676  oneqmin  7745  nlimsucg  7784  onzsl  7788  tfinds  7802  funcnvuni  7874  mptcnfimad  7930  opiota  8003  mposn  8045  frpoins3xpg  8082  frpoins3xp3g  8083  poxp2  8085  xpord2pred  8087  sexp2  8088  poxp3  8092  xpord3pred  8094  sexp3  8095  xpord3inddlem  8096  suppssov1  8139  suppssov2  8140  suppssfv  8144  brtpos  8177  frrlem12  8239  frrlem13  8240  seqomlem1  8381  seqomlem2  8382  omordi  8493  omord  8495  omwordi  8498  oeeui  8530  nnmordi  8559  nnmord  8560  nnmwordi  8563  nnawordex  8565  nnaordex  8566  nneob  8584  omsmolem  8585  eldifsucnn  8592  qsss  8713  eroveu  8749  mapsncnv  8831  ralxpmap  8834  elixpsn  8875  ixpsnf1o  8876  boxcutc  8879  pw2f1olem  9009  2pwne  9061  mapxpen  9071  mapunen  9074  php  9131  onomeneq  9138  unxpdomlem2  9157  en1eqsnbi  9176  isfiniteg  9200  fofinf1o  9232  f1opwfi  9256  elfiun  9333  oieu  9444  brwdom2  9478  wdomtr  9480  ixpiunwdom  9495  en3lplem1  9521  suc11reg  9528  inf3lemd  9536  cantnfvalf  9574  cantnflt  9581  cantnfp1lem3  9589  cantnflem2  9599  ttrcltr  9625  rnttrcl  9631  ttrclselem1  9634  r1tr  9688  updjud  9846  dfac8alem  9939  wdomnumr  9974  isinfcard  10002  aceq3lem  10030  dfac5lem4  10036  dfac5lem4OLD  10038  dfac5  10039  dfac2b  10041  coftr  10183  fin23lem28  10250  fin23lem29  10251  fin1a2lem11  10320  fin1a2lem12  10321  fin1a2lem13  10322  hsmexlem9  10335  axdclem  10429  pwcfsdom  10494  gchdomtri  10540  fpwwe2  10554  gchpwdom  10581  gchhar  10590  addnidpi  10812  nqereu  10840  genpv  10910  genpdm  10913  distrlem5pr  10938  mulrid  11130  ltne  11230  mul02  11311  cnegex  11314  mul0or  11777  negfi  12091  sup2  12098  supaddc  12109  supadd  12110  supmul1  12111  supmul  12114  creur  12139  creui  12140  cju  12141  nnsub  12189  un0addcl  12434  un0mulcl  12435  nn0sub  12451  elz2  12506  zaddcl  12531  suprzcl2  12851  qmulz  12864  qre  12866  qnegcl  12879  elpqb  12889  xrmax1  13090  xrmin2  13093  max1ALT  13101  xlesubadd  13178  xmulass  13202  xlemul1a  13203  xrsupexmnf  13220  xrinfmexpnf  13221  xrub  13227  iccid  13306  fzsn  13482  fzsuc2  13498  fz1sbc  13516  elfzp12  13519  modmuladd  13836  seqid3  13969  bcval5  14241  bcpasc  14244  hashbnd  14259  hashnnn0genn0  14266  hashprg  14318  hashfzo  14352  tpfo  14423  wrdl1s1  14538  ccats1alpha  14543  cats1un  14644  s7f1o  14889  shftlem  14991  replim  15039  absmod0  15226  absz  15234  rlimdm  15474  summolem2  15639  summo  15640  zsum  15641  fsum  15643  fsummulc2  15707  fsumconst  15713  fsum00  15721  incexclem  15759  isumsplit  15763  infcvgaux1i  15780  prodmolem2  15858  prodmo  15859  zprod  15860  fprod  15864  prodsn  15885  prodsnf  15887  fprodconst  15901  ruclem2  16157  fzo0dvdseq  16250  bitsf1ocnv  16371  sadcaddlem  16384  smueqlem  16417  gcdabs1  16456  bezoutlem1  16466  bezoutlem3  16468  bezoutlem4  16469  dvdsgcd  16471  dvdsmulgcd  16483  lcmgcdeq  16539  lcmf  16560  lcmfunsnlem1  16564  lcmfunsnlem2lem2  16566  isprm2lem  16608  dvdsprime  16614  isprm5  16634  coprm  16638  prmdvdsexpr  16644  rpexp  16649  phibndlem  16697  dfphi2  16701  hashgcdlem  16715  odzdvds  16723  nnoddn2prm  16739  pythagtriplem1  16744  iserodd  16763  pceulem  16773  pcqmul  16781  pcqcl  16784  pcxnn0cl  16788  pcxcl  16789  pcneg  16802  pcabs  16803  pcgcd1  16805  pcz  16809  pcprmpw2  16810  pcprmpw  16811  dvdsprmpweqle  16814  difsqpwdvds  16815  pcaddlem  16816  pcadd  16817  pcmpt  16820  pockthg  16834  prmreclem5  16848  4sqlem4  16880  mul4sq  16882  vdwapun  16902  vdwlem2  16910  vdwlem6  16914  vdwlem8  16916  vdwlem13  16921  0ram  16948  ram0  16950  ramcl  16957  cshwsiun  17027  wunress  17176  firest  17352  isssc  17744  pospo  18266  latnlej  18379  gsumval2a  18610  xpsmnd0  18703  mnd1id  18705  0subm  18742  mulgnn0p1  19015  mulgnn0ass  19040  cyccom  19132  gicsubgen  19208  symg1bas  19320  snsymgefmndeq  19324  psgnunilem1  19422  psgnunilem2  19424  mndodcongi  19472  oddvdsnn0  19473  odnncl  19474  oddvds  19476  odeq  19479  odeq1  19489  pgpfi2  19535  sylow2a  19548  sylow2blem3  19551  sylow3lem6  19561  lsmelvalm  19580  lsmsubm  19582  lsmsubg  19583  lsmmod  19604  lsmdisj2  19611  efgmnvl  19643  efgtlen  19655  efgs1b  19665  efgrelexlemb  19679  efgredeu  19681  efgcpbllemb  19684  frgpuptinv  19700  frgpup3lem  19706  qusabl  19794  frgpnabllem1  19802  cyggeninv  19812  cyggenod  19813  gsumval3eu  19833  dprdssv  19947  dprdfeq0  19953  dprdsubg  19955  dprddisj2  19970  ablfacrp  19997  pgpfac1lem3  20008  pgpfaclem2  20013  xpsring1d  20269  dvreq1  20347  irredn1  20362  nzrunit  20457  ringcinv  20604  rrgeq0  20633  domneq0  20641  drngmul0orOLD  20694  isabvd  20745  abvdom  20763  issrngd  20788  lmodfopnelem2  20850  lss1d  20914  lspsneq0  20963  lbspss  21034  lsmcl  21035  lvecvs0or  21063  lspindpi  21087  lidl1el  21181  lpiss  21284  lidldvgen  21289  qsssubdrg  21381  zringlpirlem1  21417  pzriprnglem6  21441  pzriprnglem12  21447  znfld  21515  znunit  21518  znrrg  21520  cygznlem3  21524  frgpcyg  21528  psgnghm  21535  ipeq0  21593  cssincl  21643  lsmcss  21647  obselocv  21683  dsmmacl  21696  dsmmlss  21699  mplsubrglem  21959  mplmonmul  21991  mplcoe5lem  21994  mhpsclcl  22090  mhpvarcl  22091  psdmul  22109  coe1tmmul2  22218  coe1tmmul  22219  pf1ind  22299  mat1dimelbas  22415  mdetralt  22552  mdetunilem2  22557  mdetunilem7  22562  mdetunilem9  22564  maducoeval2  22584  chpscmat  22786  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  istopon  22856  eltg3  22906  tgidm  22924  clsval2  22994  opncldf1  23028  restbas  23102  tgrest  23103  restcld  23116  restcldr  23118  restcls  23125  restntr  23126  ordtbas2  23135  ordtbas  23136  ordtrest2lem  23147  ordtrest2  23148  pnfnei  23164  mnfnei  23165  tgcn  23196  cnconst  23228  cnindis  23236  lmss  23242  ordtt1  23323  discmp  23342  1stcrest  23397  2ndcdisj  23400  cldllycmp  23439  txbas  23511  ptpjpre1  23515  ptuni2  23520  ptbasin  23521  ptbasfi  23525  ptopn2  23528  txbasval  23550  ptpjopn  23556  ptclsg  23559  dfac14lem  23561  xkoccn  23563  ptcnp  23566  upxp  23567  ptrescn  23583  txkgen  23596  xkoptsub  23598  xkopt  23599  xkoco1cn  23601  xkoco2cn  23602  xkococn  23604  xkoinjcn  23631  ordthmeolem  23745  ptuncnv  23751  nrmhaus  23770  fbssint  23782  fbfinnfr  23785  fbasrn  23828  isufil2  23852  filufint  23864  rnelfm  23897  fmfnfmlem2  23899  fmfnfmlem3  23900  fmfnfmlem4  23901  fmfnfm  23902  flimtopon  23914  flimclslem  23928  fclstopon  23956  fclscf  23969  flimfnfcls  23972  alexsublem  23988  alexsubALTlem3  23993  alexsubALTlem4  23994  ptcmplem2  23997  tmdgsum2  24040  symgtgp  24050  cldsubg  24055  qustgplem  24065  tgptsmscld  24095  tsmsxplem1  24097  imasdsf1olem  24317  blssps  24368  blss  24369  stdbdxmet  24459  methaus  24464  metrest  24468  nrginvrcn  24636  nmoeq0  24680  blssioo  24739  xrtgioo  24751  xrsxmet  24754  reconnlem1  24771  reconnlem2  24772  xrge0tsms  24779  elcncf1di  24844  iccpnfcnv  24898  evth  24914  lebnumlem1  24916  lebnumlem2  24917  lebnumlem3  24918  nmoleub3  25075  minveclem3b  25384  ivthlem2  25409  ivthlem3  25410  elovolm  25432  ovolmge0  25434  ovoliun  25462  ovolicc2lem3  25476  ovolicc2  25479  voliunlem3  25509  dyaddisj  25553  dyadmax  25555  opnmblALT  25560  ismbfd  25596  ismbf2d  25597  mbfimaopnlem  25612  mbfimaopn2  25614  i1fmullem  25651  i1fres  25662  itg1climres  25671  mbfi1fseqlem4  25675  itg2lcl  25684  itgsplitioo  25795  ellimc2  25834  rolle  25950  dvlip  25954  dvge0  25967  dvne0  25972  lhop1lem  25974  tdeglem4  26021  degltlem1  26033  deg1nn0clb  26051  deg1lt0  26052  dvdsq1p  26124  ply1rem  26127  fta1g  26131  elply2  26157  plyf  26159  ne0p  26168  plyeq0lem  26171  plypf1  26173  0dgrb  26207  coe1termlem  26219  dgrcolem2  26236  plymul0or  26244  plyrem  26269  fta1  26272  quotcan  26273  aalioulem3  26298  eff1olem  26513  lognegb  26555  eflogeq  26567  argregt0  26575  argrege0  26576  tanarg  26584  cxpexp  26633  cxpeq0  26643  mulcxp  26650  cxpeq  26723  atans2  26897  scvxcvx  26952  dmgmaddn0  26989  isppw2  27081  vmappw  27082  vmacl  27084  efvmacl  27086  isnsqf  27101  mumullem2  27146  sqff1o  27148  dvdsppwf1o  27152  ppiublem1  27169  vmalelog  27172  chtublem  27178  fsumvma  27180  perfectlem2  27197  perfect  27198  bposlem1  27251  lgsmod  27290  lgsne0  27302  lgsdirnn0  27311  lgsqr  27318  lgsdchr  27322  gausslemma2dlem1a  27332  gausslemma2dlem6  27339  lgseisenlem2  27343  lgsquadlem1  27347  lgsquadlem2  27348  2lgslem1b  27359  2sqlem2  27385  mul2sq  27386  2sqlem7  27391  dchrisum0fno1  27478  pntrsumbnd2  27534  ostthlem1  27594  ostth2lem2  27601  ostth3  27605  ostth  27606  nolesgn2ores  27640  nogesgn1ores  27642  nolt02o  27663  nogt01o  27664  nosupbnd2  27684  noinfbnd2lem1  27698  noetasuplem4  27704  noetainflem4  27708  maxs1  27737  mins2  27740  ltsne  27742  eqcuts3  27800  cuteq1  27813  madef  27832  ltslpss  27904  lrrecfr  27939  addsval  27958  addsproplem2  27966  addsuniflem  27997  addbdaylem  28013  negsid  28037  negsunif  28051  mulsproplem5  28116  mulsproplem6  28117  mulsproplem7  28118  mulsproplem8  28119  mulsproplem9  28120  lemulsd  28134  sltmuls1  28143  sltmuls2  28144  ltmuls2  28167  muls0ord  28181  precsexlem8  28210  precsexlem9  28211  precsexlem11  28213  elons2  28254  oncutlt  28260  bdayons  28272  onaddscl  28273  onmulscl  28274  nnsge1  28339  n0fincut  28351  n0subs  28359  dfnns2  28368  eucliddivs  28372  znegscl  28388  zaddscl  28390  zmulscld  28393  elzn0s  28394  eln0zs  28396  n0seo  28417  zseo  28418  bdaypw2n0bndlem  28459  bdaypw2n0bnd  28460  z12no  28472  z12addscl  28473  z12negscl  28474  z12shalf  28476  z12zsodd  28478  z12sge0  28479  z12bdaylem  28480  bdayfinlem  28482  recut  28490  elreno2  28491  remulscllem1  28496  colinearalg  28983  axpasch  29014  axlowdimlem16  29030  axlowdimlem17  29031  axlowdim  29034  axcontlem2  29038  axcontlem4  29040  axcontlem7  29043  lpvtx  29141  edglnl  29216  numedglnl  29217  usgredgop  29243  usgrexmplef  29332  uhgrspansubgrlem  29363  uhgrspan1  29376  nbusgredgeu0  29441  nb3grprlem2  29454  cusgrsize2inds  29527  vtxd0nedgb  29562  rusgrpropnb  29657  upgrwlkvtxedg  29718  wlkp1lem1  29745  wlkp1lem6  29750  wlkp1lem8  29752  usgr2wlkneq  29829  crctcshwlk  29895  crctcsh  29897  iswwlksnon  29926  wlkiswwlks1  29940  wwlksnextbi  29967  wwlksnextproplem2  29983  wspthsnonn0vne  29990  clwlkclwwlklem2  30075  clwwisshclwws  30090  erclwwlktr  30097  clwwlkel  30121  clwwlkext2edg  30131  erclwwlkntr  30146  clwlknf1oclwwlknlem2  30157  clwlknf1oclwwlknlem3  30158  clwlknf1oclwwlkn  30159  clwwlknonccat  30171  0wlkons1  30196  3wlkdlem6  30240  eupth2eucrct  30292  frgrwopreglem2  30388  2clwwlk2clwwlk  30425  wlkl0  30442  nvmul0or  30725  ipasslem5  30910  ipasslem11  30915  hvmul0or  31100  his6  31174  hhssnv  31339  ocsh  31358  ocin  31371  shsidmi  31459  chnlen0  31519  h1de2bi  31629  h1de2ctlem  31630  h1de2ci  31631  spansni  31632  3oalem1  31737  nmcexi  32101  atcveq0  32423  chcv1  32430  cdjreui  32507  cdj3lem2b  32512  xrge0tsmsd  33155  1fldgenq  33404  ccfldextdgrr  33829  ordtrest2NEWlem  34079  ordtrest2NEW  34080  xrge0iifcnv  34090  esumc  34208  esumpcvgval  34235  ballotlemfc0  34650  ballotlemfcc  34651  fissorduni  35246  fineqvnttrclse  35280  gblacfnacd  35296  subfacp1lem4  35377  subfacp1lem5  35378  erdszelem8  35392  sconnpi1  35433  cvmsss2  35468  cvmlift2lem12  35508  satfv0  35552  satfv0fun  35565  satf00  35568  sat1el2xp  35573  fmla0xp  35577  fmlasucdisj  35593  satffunlem1lem1  35596  satffunlem2lem1  35598  dmopab3rexdif  35599  msubco  35725  msubvrs  35754  ellcsrspsn  35835  sinccvglem  35866  untsucf  35904  nnuni  35921  dfrdg2  35987  colineardim1  36255  btwnconn1lem14  36294  segleantisym  36309  colinbtwnle  36312  outsidele  36326  lineunray  36341  linethru  36347  elicc3  36511  opnregcld  36524  cldregopn  36525  fnejoin2  36563  bj-isrvec  37499  dissneqlem  37545  icorempo  37556  relowlssretop  37568  relowlpssretop  37569  rdgssun  37583  finxpsuclem  37602  lindsenlbs  37816  ptrecube  37821  poimirlem6  37827  poimirlem7  37828  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem21  37842  poimirlem22  37843  poimirlem23  37844  poimirlem24  37845  poimirlem25  37846  poimirlem26  37847  poimirlem27  37848  poimirlem29  37850  poimirlem30  37851  poimirlem31  37852  poimirlem32  37853  itg2addnclem3  37874  ftc1anclem6  37899  dvasin  37905  unirep  37915  sdclem2  37943  ssbnd  37989  prdsbnd  37994  cntotbnd  37997  heibor1lem  38010  rrnequiv  38036  ismndo2  38075  grpoeqdivid  38082  isdrngo3  38160  crngohomfo  38207  0idl  38226  1idl  38227  divrngidl  38229  smprngopr  38253  prnc  38268  ispridlc  38271  riotaclbgBAD  39214  lshpdisj  39247  lsateln0  39255  lsatcveq0  39292  opnlen0  39448  cmtbr4N  39515  cvrnbtwn2  39535  cvrnbtwn4  39539  atcvreq0  39574  cvlatexch1  39596  exatleN  39664  atlelt  39698  ps-2  39738  llnn0  39776  lplnn0N  39807  islpln2a  39808  lvoln0N  39851  islvol2aN  39852  4at  39873  dalemcea  39920  dalem3  39924  pmapglb2N  40031  pmapglb2xN  40032  cdlema1N  40051  cdlemb  40054  paddasslem17  40096  llnexchb2lem  40128  llnexchb2  40129  lhpat3  40306  ltrnid  40395  trlne  40445  cdlemc4  40454  cdleme11h  40526  cdlemednuN  40560  cdlemg1a  40830  tendoeq2  41034  tendoid0  41085  dva1dim  41245  dib1dim  41425  dihlatat  41597  dochkrshp4  41649  dochkr1  41738  lclkrlem2e  41771  lcfrlem16  41818  lcfrlem28  41830  mapd0  41925  hdmap14lem13  42140  eqresfnbd  42488  f1o2d2  42489  expeq1d  42579  expeqidd  42580  dvdsexpnn0  42589  reladdrsub  42640  sn-remul0ord  42663  sn-negex12  42672  sn-mullid  42691  sn-mul02  42707  nn0addcom  42717  nn0mulcom  42721  zmulcomlem  42722  mulgt0con1d  42725  mulgt0con2d  42726  sn-sup2  42746  frlmsnic  42795  evlselvlem  42829  prjspner1  42869  elrfi  42936  mrefg2  42949  eldiophb  42999  eldioph2b  43005  diophin  43014  diophun  43015  rexzrexnn0  43046  eldioph4b  43053  diophren  43055  rencldnfilem  43062  pellexlem6  43076  jm2.19  43235  rmydioph  43256  expdiophlem1  43263  expdioph  43265  lnr2i  43358  lpirlnr  43359  hbtlem2  43366  hbtlem4  43368  hbtlem6  43371  dgrsub2  43377  dgraa0p  43391  rngunsnply  43411  nlimsuc  43682  dfsucon  43764  radcnvrat  44555  pm14.24  44673  addrcom  44715  modelaxreplem1  45219  ormklocald  47118  natlocalincr  47120  afveu  47399  dfafn5b  47407  rlimdmafv  47423  afv2eu  47484  rlimdmafv2  47504  el1fzopredsuc  47571  minusmod5ne  47595  modmknepk  47608  elsetpreimafvssdm  47632  imasetpreimafvbijlemfo  47651  sprvalpw  47726  prprvalpw  47761  reupr  47768  fmtnofac2lem  47814  proththdlem  47859  perfectALTVlem2  47968  perfectALTV  47969  gbowpos  48005  gbowgt5  48008  gboge9  48010  nnsum4primesodd  48042  nnsum4primesoddALTV  48043  uhgrimedgi  48136  isuspgrim0  48140  isuspgrimlem  48141  upgrimpths  48155  clnbgrgrim  48180  grimedg  48181  grtrissvtx  48190  stgredgiun  48204  stgrvtx0  48208  isubgr3stgrlem7  48218  grlimgrtrilem2  48248  gpgiedgdmellem  48292  gpgvtxel2  48294  gpgvtx0  48299  gpgvtx1  48300  gpgusgralem  48302  gpgedgvtx0  48307  gpgedgvtx1  48308  gpgedg2ov  48312  gpgedg2iv  48313  gpgnbgrvtx0  48320  gpgnbgrvtx1  48321  pgnbgreunbgr  48371  ringcinvALTV  48556  lincellss  48672  lindsrng01  48714  suppdm  48756  nnpw2pb  48833  0aryfvalel  48880  0aryfvalelfv  48881  itsclc0xyqsolr  49015  infsubc  49305  infsubc2  49306