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  4494  elsn2g  4623  preq1b  4804  elpreqprb  4826  reusv3  5352  alxfr  5354  reuhypd  5366  axpr  5374  opth1  5431  euotd  5469  otiunsndisj  5476  tz7.2  5615  frsn  5720  dmopab2rex  5874  elsnxp  6257  reuop  6259  dfpo2  6262  ordtri1  6358  ordtri3  6361  fvmptdv2  6968  fveqressseq  7033  foco2  7063  fsn  7090  fnsnbg  7120  fnsnbOLD  7122  fmptsng  7124  fmptsnd  7125  fconst2g  7159  fnprb  7164  fntpb  7165  funfvima  7186  soisoi  7284  isores3  7291  eqfunresadj  7316  riotaeqimp  7351  eusvobj2  7360  ovmpodv2  7526  f1opw2  7623  sorpssun  7685  sorpssin  7686  oneqmin  7755  nlimsucg  7794  onzsl  7798  tfinds  7812  funcnvuni  7884  mptcnfimad  7940  opiota  8013  mposn  8055  frpoins3xpg  8092  frpoins3xp3g  8093  poxp2  8095  xpord2pred  8097  sexp2  8098  poxp3  8102  xpord3pred  8104  sexp3  8105  xpord3inddlem  8106  suppssov1  8149  suppssov2  8150  suppssfv  8154  brtpos  8187  frrlem12  8249  frrlem13  8250  seqomlem1  8391  seqomlem2  8392  omordi  8503  omord  8505  omwordi  8508  oeeui  8540  nnmordi  8569  nnmord  8570  nnmwordi  8573  nnawordex  8575  nnaordex  8576  nneob  8594  omsmolem  8595  eldifsucnn  8602  qsss  8724  eroveu  8761  mapsncnv  8843  ralxpmap  8846  elixpsn  8887  ixpsnf1o  8888  boxcutc  8891  pw2f1olem  9021  2pwne  9073  mapxpen  9083  mapunen  9086  php  9143  onomeneq  9150  unxpdomlem2  9169  en1eqsnbi  9188  isfiniteg  9212  fofinf1o  9244  f1opwfi  9268  elfiun  9345  oieu  9456  brwdom2  9490  wdomtr  9492  ixpiunwdom  9507  en3lplem1  9533  suc11reg  9540  inf3lemd  9548  cantnfvalf  9586  cantnflt  9593  cantnfp1lem3  9601  cantnflem2  9611  ttrcltr  9637  rnttrcl  9643  ttrclselem1  9646  r1tr  9700  updjud  9858  dfac8alem  9951  wdomnumr  9986  isinfcard  10014  aceq3lem  10042  dfac5lem4  10048  dfac5lem4OLD  10050  dfac5  10051  dfac2b  10053  coftr  10195  fin23lem28  10262  fin23lem29  10263  fin1a2lem11  10332  fin1a2lem12  10333  fin1a2lem13  10334  hsmexlem9  10347  axdclem  10441  pwcfsdom  10506  gchdomtri  10552  fpwwe2  10566  gchpwdom  10593  gchhar  10602  addnidpi  10824  nqereu  10852  genpv  10922  genpdm  10925  distrlem5pr  10950  mulrid  11142  ltne  11242  mul02  11323  cnegex  11326  mul0or  11789  negfi  12103  sup2  12110  supaddc  12121  supadd  12122  supmul1  12123  supmul  12126  creur  12151  creui  12152  cju  12153  nnsub  12201  un0addcl  12446  un0mulcl  12447  nn0sub  12463  elz2  12518  zaddcl  12543  suprzcl2  12863  qmulz  12876  qre  12878  qnegcl  12891  elpqb  12901  xrmax1  13102  xrmin2  13105  max1ALT  13113  xlesubadd  13190  xmulass  13214  xlemul1a  13215  xrsupexmnf  13232  xrinfmexpnf  13233  xrub  13239  iccid  13318  fzsn  13494  fzsuc2  13510  fz1sbc  13528  elfzp12  13531  modmuladd  13848  seqid3  13981  bcval5  14253  bcpasc  14256  hashbnd  14271  hashnnn0genn0  14278  hashprg  14330  hashfzo  14364  tpfo  14435  wrdl1s1  14550  ccats1alpha  14555  cats1un  14656  s7f1o  14901  shftlem  15003  replim  15051  absmod0  15238  absz  15246  rlimdm  15486  summolem2  15651  summo  15652  zsum  15653  fsum  15655  fsummulc2  15719  fsumconst  15725  fsum00  15733  incexclem  15771  isumsplit  15775  infcvgaux1i  15792  prodmolem2  15870  prodmo  15871  zprod  15872  fprod  15876  prodsn  15897  prodsnf  15899  fprodconst  15913  ruclem2  16169  fzo0dvdseq  16262  bitsf1ocnv  16383  sadcaddlem  16396  smueqlem  16429  gcdabs1  16468  bezoutlem1  16478  bezoutlem3  16480  bezoutlem4  16481  dvdsgcd  16483  dvdsmulgcd  16495  lcmgcdeq  16551  lcmf  16572  lcmfunsnlem1  16576  lcmfunsnlem2lem2  16578  isprm2lem  16620  dvdsprime  16626  isprm5  16646  coprm  16650  prmdvdsexpr  16656  rpexp  16661  phibndlem  16709  dfphi2  16713  hashgcdlem  16727  odzdvds  16735  nnoddn2prm  16751  pythagtriplem1  16756  iserodd  16775  pceulem  16785  pcqmul  16793  pcqcl  16796  pcxnn0cl  16800  pcxcl  16801  pcneg  16814  pcabs  16815  pcgcd1  16817  pcz  16821  pcprmpw2  16822  pcprmpw  16823  dvdsprmpweqle  16826  difsqpwdvds  16827  pcaddlem  16828  pcadd  16829  pcmpt  16832  pockthg  16846  prmreclem5  16860  4sqlem4  16892  mul4sq  16894  vdwapun  16914  vdwlem2  16922  vdwlem6  16926  vdwlem8  16928  vdwlem13  16933  0ram  16960  ram0  16962  ramcl  16969  cshwsiun  17039  wunress  17188  firest  17364  isssc  17756  pospo  18278  latnlej  18391  gsumval2a  18622  xpsmnd0  18715  mnd1id  18717  0subm  18754  mulgnn0p1  19027  mulgnn0ass  19052  cyccom  19144  gicsubgen  19220  symg1bas  19332  snsymgefmndeq  19336  psgnunilem1  19434  psgnunilem2  19436  mndodcongi  19484  oddvdsnn0  19485  odnncl  19486  oddvds  19488  odeq  19491  odeq1  19501  pgpfi2  19547  sylow2a  19560  sylow2blem3  19563  sylow3lem6  19573  lsmelvalm  19592  lsmsubm  19594  lsmsubg  19595  lsmmod  19616  lsmdisj2  19623  efgmnvl  19655  efgtlen  19667  efgs1b  19677  efgrelexlemb  19691  efgredeu  19693  efgcpbllemb  19696  frgpuptinv  19712  frgpup3lem  19718  qusabl  19806  frgpnabllem1  19814  cyggeninv  19824  cyggenod  19825  gsumval3eu  19845  dprdssv  19959  dprdfeq0  19965  dprdsubg  19967  dprddisj2  19982  ablfacrp  20009  pgpfac1lem3  20020  pgpfaclem2  20025  xpsring1d  20281  dvreq1  20359  irredn1  20374  nzrunit  20469  ringcinv  20616  rrgeq0  20645  domneq0  20653  drngmul0orOLD  20706  isabvd  20757  abvdom  20775  issrngd  20800  lmodfopnelem2  20862  lss1d  20926  lspsneq0  20975  lbspss  21046  lsmcl  21047  lvecvs0or  21075  lspindpi  21099  lidl1el  21193  lpiss  21296  lidldvgen  21301  qsssubdrg  21393  zringlpirlem1  21429  pzriprnglem6  21453  pzriprnglem12  21459  znfld  21527  znunit  21530  znrrg  21532  cygznlem3  21536  frgpcyg  21540  psgnghm  21547  ipeq0  21605  cssincl  21655  lsmcss  21659  obselocv  21695  dsmmacl  21708  dsmmlss  21711  mplsubrglem  21971  mplmonmul  22003  mplcoe5lem  22006  mhpsclcl  22102  mhpvarcl  22103  psdmul  22121  coe1tmmul2  22230  coe1tmmul  22231  pf1ind  22311  mat1dimelbas  22427  mdetralt  22564  mdetunilem2  22569  mdetunilem7  22574  mdetunilem9  22576  maducoeval2  22596  chpscmat  22798  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  istopon  22868  eltg3  22918  tgidm  22936  clsval2  23006  opncldf1  23040  restbas  23114  tgrest  23115  restcld  23128  restcldr  23130  restcls  23137  restntr  23138  ordtbas2  23147  ordtbas  23148  ordtrest2lem  23159  ordtrest2  23160  pnfnei  23176  mnfnei  23177  tgcn  23208  cnconst  23240  cnindis  23248  lmss  23254  ordtt1  23335  discmp  23354  1stcrest  23409  2ndcdisj  23412  cldllycmp  23451  txbas  23523  ptpjpre1  23527  ptuni2  23532  ptbasin  23533  ptbasfi  23537  ptopn2  23540  txbasval  23562  ptpjopn  23568  ptclsg  23571  dfac14lem  23573  xkoccn  23575  ptcnp  23578  upxp  23579  ptrescn  23595  txkgen  23608  xkoptsub  23610  xkopt  23611  xkoco1cn  23613  xkoco2cn  23614  xkococn  23616  xkoinjcn  23643  ordthmeolem  23757  ptuncnv  23763  nrmhaus  23782  fbssint  23794  fbfinnfr  23797  fbasrn  23840  isufil2  23864  filufint  23876  rnelfm  23909  fmfnfmlem2  23911  fmfnfmlem3  23912  fmfnfmlem4  23913  fmfnfm  23914  flimtopon  23926  flimclslem  23940  fclstopon  23968  fclscf  23981  flimfnfcls  23984  alexsublem  24000  alexsubALTlem3  24005  alexsubALTlem4  24006  ptcmplem2  24009  tmdgsum2  24052  symgtgp  24062  cldsubg  24067  qustgplem  24077  tgptsmscld  24107  tsmsxplem1  24109  imasdsf1olem  24329  blssps  24380  blss  24381  stdbdxmet  24471  methaus  24476  metrest  24480  nrginvrcn  24648  nmoeq0  24692  blssioo  24751  xrtgioo  24763  xrsxmet  24766  reconnlem1  24783  reconnlem2  24784  xrge0tsms  24791  elcncf1di  24856  iccpnfcnv  24910  evth  24926  lebnumlem1  24928  lebnumlem2  24929  lebnumlem3  24930  nmoleub3  25087  minveclem3b  25396  ivthlem2  25421  ivthlem3  25422  elovolm  25444  ovolmge0  25446  ovoliun  25474  ovolicc2lem3  25488  ovolicc2  25491  voliunlem3  25521  dyaddisj  25565  dyadmax  25567  opnmblALT  25572  ismbfd  25608  ismbf2d  25609  mbfimaopnlem  25624  mbfimaopn2  25626  i1fmullem  25663  i1fres  25674  itg1climres  25683  mbfi1fseqlem4  25687  itg2lcl  25696  itgsplitioo  25807  ellimc2  25846  rolle  25962  dvlip  25966  dvge0  25979  dvne0  25984  lhop1lem  25986  tdeglem4  26033  degltlem1  26045  deg1nn0clb  26063  deg1lt0  26064  dvdsq1p  26136  ply1rem  26139  fta1g  26143  elply2  26169  plyf  26171  ne0p  26180  plyeq0lem  26183  plypf1  26185  0dgrb  26219  coe1termlem  26231  dgrcolem2  26248  plymul0or  26256  plyrem  26281  fta1  26284  quotcan  26285  aalioulem3  26310  eff1olem  26525  lognegb  26567  eflogeq  26579  argregt0  26587  argrege0  26588  tanarg  26596  cxpexp  26645  cxpeq0  26655  mulcxp  26662  cxpeq  26735  atans2  26909  scvxcvx  26964  dmgmaddn0  27001  isppw2  27093  vmappw  27094  vmacl  27096  efvmacl  27098  isnsqf  27113  mumullem2  27158  sqff1o  27160  dvdsppwf1o  27164  ppiublem1  27181  vmalelog  27184  chtublem  27190  fsumvma  27192  perfectlem2  27209  perfect  27210  bposlem1  27263  lgsmod  27302  lgsne0  27314  lgsdirnn0  27323  lgsqr  27330  lgsdchr  27334  gausslemma2dlem1a  27344  gausslemma2dlem6  27351  lgseisenlem2  27355  lgsquadlem1  27359  lgsquadlem2  27360  2lgslem1b  27371  2sqlem2  27397  mul2sq  27398  2sqlem7  27403  dchrisum0fno1  27490  pntrsumbnd2  27546  ostthlem1  27606  ostth2lem2  27613  ostth3  27617  ostth  27618  nolesgn2ores  27652  nogesgn1ores  27654  nolt02o  27675  nogt01o  27676  nosupbnd2  27696  noinfbnd2lem1  27710  noetasuplem4  27716  noetainflem4  27720  maxs1  27749  mins2  27752  ltsne  27754  eqcuts3  27812  cuteq1  27825  madef  27844  ltslpss  27916  lrrecfr  27951  addsval  27970  addsproplem2  27978  addsuniflem  28009  addbdaylem  28025  negsid  28049  negsunif  28063  mulsproplem5  28128  mulsproplem6  28129  mulsproplem7  28130  mulsproplem8  28131  mulsproplem9  28132  lemulsd  28146  sltmuls1  28155  sltmuls2  28156  ltmuls2  28179  muls0ord  28193  precsexlem8  28222  precsexlem9  28223  precsexlem11  28225  elons2  28266  oncutlt  28272  bdayons  28284  onaddscl  28285  onmulscl  28286  nnsge1  28351  n0fincut  28363  n0subs  28371  dfnns2  28380  eucliddivs  28384  znegscl  28400  zaddscl  28402  zmulscld  28405  elzn0s  28406  eln0zs  28408  n0seo  28429  zseo  28430  bdaypw2n0bndlem  28471  bdaypw2n0bnd  28472  z12no  28484  z12addscl  28485  z12negscl  28486  z12shalf  28488  z12zsodd  28490  z12sge0  28491  z12bdaylem  28492  bdayfinlem  28494  recut  28502  elreno2  28503  remulscllem1  28508  colinearalg  28995  axpasch  29026  axlowdimlem16  29042  axlowdimlem17  29043  axlowdim  29046  axcontlem2  29050  axcontlem4  29052  axcontlem7  29055  lpvtx  29153  edglnl  29228  numedglnl  29229  usgredgop  29255  usgrexmplef  29344  uhgrspansubgrlem  29375  uhgrspan1  29388  nbusgredgeu0  29453  nb3grprlem2  29466  cusgrsize2inds  29539  vtxd0nedgb  29574  rusgrpropnb  29669  upgrwlkvtxedg  29730  wlkp1lem1  29757  wlkp1lem6  29762  wlkp1lem8  29764  usgr2wlkneq  29841  crctcshwlk  29907  crctcsh  29909  iswwlksnon  29938  wlkiswwlks1  29952  wwlksnextbi  29979  wwlksnextproplem2  29995  wspthsnonn0vne  30002  clwlkclwwlklem2  30087  clwwisshclwws  30102  erclwwlktr  30109  clwwlkel  30133  clwwlkext2edg  30143  erclwwlkntr  30158  clwlknf1oclwwlknlem2  30169  clwlknf1oclwwlknlem3  30170  clwlknf1oclwwlkn  30171  clwwlknonccat  30183  0wlkons1  30208  3wlkdlem6  30252  eupth2eucrct  30304  frgrwopreglem2  30400  2clwwlk2clwwlk  30437  wlkl0  30454  nvmul0or  30738  ipasslem5  30923  ipasslem11  30928  hvmul0or  31113  his6  31187  hhssnv  31352  ocsh  31371  ocin  31384  shsidmi  31472  chnlen0  31532  h1de2bi  31642  h1de2ctlem  31643  h1de2ci  31644  spansni  31645  3oalem1  31750  nmcexi  32114  atcveq0  32436  chcv1  32443  cdjreui  32520  cdj3lem2b  32525  xrge0tsmsd  33167  1fldgenq  33416  psrmonmul  33727  ccfldextdgrr  33850  ordtrest2NEWlem  34100  ordtrest2NEW  34101  xrge0iifcnv  34111  esumc  34229  esumpcvgval  34256  ballotlemfc0  34671  ballotlemfcc  34672  fissorduni  35267  axprALT2  35287  fineqvnttrclse  35302  gblacfnacd  35318  subfacp1lem4  35399  subfacp1lem5  35400  erdszelem8  35414  sconnpi1  35455  cvmsss2  35490  cvmlift2lem12  35530  satfv0  35574  satfv0fun  35587  satf00  35590  sat1el2xp  35595  fmla0xp  35599  fmlasucdisj  35615  satffunlem1lem1  35618  satffunlem2lem1  35620  dmopab3rexdif  35621  msubco  35747  msubvrs  35776  ellcsrspsn  35857  sinccvglem  35888  untsucf  35926  nnuni  35943  dfrdg2  36009  colineardim1  36277  btwnconn1lem14  36316  segleantisym  36331  colinbtwnle  36334  outsidele  36348  lineunray  36363  linethru  36369  elicc3  36533  opnregcld  36546  cldregopn  36547  fnejoin2  36585  bj-isrvec  37549  dissneqlem  37595  icorempo  37606  relowlssretop  37618  relowlpssretop  37619  rdgssun  37633  finxpsuclem  37652  lindsenlbs  37866  ptrecube  37871  poimirlem6  37877  poimirlem7  37878  poimirlem16  37887  poimirlem17  37888  poimirlem19  37890  poimirlem20  37891  poimirlem21  37892  poimirlem22  37893  poimirlem23  37894  poimirlem24  37895  poimirlem25  37896  poimirlem26  37897  poimirlem27  37898  poimirlem29  37900  poimirlem30  37901  poimirlem31  37902  poimirlem32  37903  itg2addnclem3  37924  ftc1anclem6  37949  dvasin  37955  unirep  37965  sdclem2  37993  ssbnd  38039  prdsbnd  38044  cntotbnd  38047  heibor1lem  38060  rrnequiv  38086  ismndo2  38125  grpoeqdivid  38132  isdrngo3  38210  crngohomfo  38257  0idl  38276  1idl  38277  divrngidl  38279  smprngopr  38303  prnc  38318  ispridlc  38321  disjimeceqim  39055  riotaclbgBAD  39330  lshpdisj  39363  lsateln0  39371  lsatcveq0  39408  opnlen0  39564  cmtbr4N  39631  cvrnbtwn2  39651  cvrnbtwn4  39655  atcvreq0  39690  cvlatexch1  39712  exatleN  39780  atlelt  39814  ps-2  39854  llnn0  39892  lplnn0N  39923  islpln2a  39924  lvoln0N  39967  islvol2aN  39968  4at  39989  dalemcea  40036  dalem3  40040  pmapglb2N  40147  pmapglb2xN  40148  cdlema1N  40167  cdlemb  40170  paddasslem17  40212  llnexchb2lem  40244  llnexchb2  40245  lhpat3  40422  ltrnid  40511  trlne  40561  cdlemc4  40570  cdleme11h  40642  cdlemednuN  40676  cdlemg1a  40946  tendoeq2  41150  tendoid0  41201  dva1dim  41361  dib1dim  41541  dihlatat  41713  dochkrshp4  41765  dochkr1  41854  lclkrlem2e  41887  lcfrlem16  41934  lcfrlem28  41946  mapd0  42041  hdmap14lem13  42256  eqresfnbd  42604  f1o2d2  42605  expeq1d  42694  expeqidd  42695  dvdsexpnn0  42704  reladdrsub  42755  sn-remul0ord  42778  sn-negex12  42787  sn-mullid  42806  sn-mul02  42822  nn0addcom  42832  nn0mulcom  42836  zmulcomlem  42837  mulgt0con1d  42840  mulgt0con2d  42841  sn-sup2  42861  frlmsnic  42910  evlselvlem  42944  prjspner1  42984  elrfi  43051  mrefg2  43064  eldiophb  43114  eldioph2b  43120  diophin  43129  diophun  43130  rexzrexnn0  43161  eldioph4b  43168  diophren  43170  rencldnfilem  43177  pellexlem6  43191  jm2.19  43350  rmydioph  43371  expdiophlem1  43378  expdioph  43380  lnr2i  43473  lpirlnr  43474  hbtlem2  43481  hbtlem4  43483  hbtlem6  43486  dgrsub2  43492  dgraa0p  43506  rngunsnply  43526  nlimsuc  43797  dfsucon  43879  radcnvrat  44670  pm14.24  44788  addrcom  44830  modelaxreplem1  45334  ormklocald  47232  natlocalincr  47234  afveu  47513  dfafn5b  47521  rlimdmafv  47537  afv2eu  47598  rlimdmafv2  47618  el1fzopredsuc  47685  minusmod5ne  47709  modmknepk  47722  elsetpreimafvssdm  47746  imasetpreimafvbijlemfo  47765  sprvalpw  47840  prprvalpw  47875  reupr  47882  fmtnofac2lem  47928  proththdlem  47973  perfectALTVlem2  48082  perfectALTV  48083  gbowpos  48119  gbowgt5  48122  gboge9  48124  nnsum4primesodd  48156  nnsum4primesoddALTV  48157  uhgrimedgi  48250  isuspgrim0  48254  isuspgrimlem  48255  upgrimpths  48269  clnbgrgrim  48294  grimedg  48295  grtrissvtx  48304  stgredgiun  48318  stgrvtx0  48322  isubgr3stgrlem7  48332  grlimgrtrilem2  48362  gpgiedgdmellem  48406  gpgvtxel2  48408  gpgvtx0  48413  gpgvtx1  48414  gpgusgralem  48416  gpgedgvtx0  48421  gpgedgvtx1  48422  gpgedg2ov  48426  gpgedg2iv  48427  gpgnbgrvtx0  48434  gpgnbgrvtx1  48435  pgnbgreunbgr  48485  ringcinvALTV  48670  lincellss  48786  lindsrng01  48828  suppdm  48870  nnpw2pb  48947  0aryfvalel  48994  0aryfvalelfv  48995  itsclc0xyqsolr  49129  infsubc  49419  infsubc2  49420