Theorem syl5ibrcom 248

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  biimprcd  251  iftrueb  4467  elsn2g  4596  preq1b  4777  elpreqprb  4799  reusv3  5334  alxfr  5336  reuhypd  5348  axpr  5356  opth1  5415  euotd  5454  otiunsndisj  5461  tz7.2  5601  frsn  5706  dmopab2rex  5859  elsnxp  6242  reuop  6244  dfpo2  6247  ordtri1  6343  ordtri3  6346  fvmptdv2  6954  fveqressseq  7020  foco2  7050  fsn  7077  fnsnbg  7108  fnsnbOLD  7110  fmptsng  7112  fmptsnd  7113  fconst2g  7147  fnprb  7152  fntpb  7153  funfvima  7174  soisoi  7272  isores3  7279  eqfunresadj  7304  riotaeqimp  7339  eusvobj2  7348  ovmpodv2  7514  f1opw2  7611  sorpssun  7673  sorpssin  7674  oneqmin  7743  nlimsucg  7782  onzsl  7786  tfinds  7800  funcnvuni  7872  mptcnfimad  7928  opiota  8001  mposn  8042  mpof1o2d  8065  frpoins3xpg  8080  frpoins3xp3g  8081  poxp2  8083  xpord2pred  8085  sexp2  8086  poxp3  8090  xpord3pred  8092  sexp3  8093  xpord3inddlem  8094  suppssov1  8137  suppssov2  8138  suppssfv  8142  brtpos  8175  frrlem12  8237  frrlem13  8238  seqomlem1  8379  seqomlem2  8380  omordi  8491  omord  8493  omwordi  8496  oeeui  8528  nnmordi  8557  nnmord  8558  nnmwordi  8561  nnawordex  8563  nnaordex  8564  nneob  8582  omsmolem  8583  eldifsucnn  8590  qsss  8712  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  9524  suc11reg  9531  inf3lemd  9539  cantnfvalf  9577  cantnflt  9584  cantnfp1lem3  9592  cantnflem2  9602  ttrcltr  9628  rnttrcl  9634  ttrclselem1  9637  r1tr  9691  updjud  9849  dfac8alem  9942  wdomnumr  9977  isinfcard  10005  aceq3lem  10033  dfac5lem4  10039  dfac5lem4OLD  10041  dfac5  10042  dfac2b  10044  coftr  10186  fin23lem28  10253  fin23lem29  10254  fin1a2lem11  10323  fin1a2lem12  10324  fin1a2lem13  10325  hsmexlem9  10338  axdclem  10432  pwcfsdom  10497  gchdomtri  10543  fpwwe2  10557  gchpwdom  10584  gchhar  10593  addnidpi  10815  nqereu  10843  genpv  10913  genpdm  10916  distrlem5pr  10941  mulrid  11133  ltne  11234  mul02  11315  cnegex  11318  mul0or  11781  negfi  12096  sup2  12103  supaddc  12114  supadd  12115  supmul1  12116  supmul  12119  creur  12144  creui  12145  cju  12146  nnsub  12212  un0addcl  12461  un0mulcl  12462  nn0sub  12478  elz2  12533  zaddcl  12558  suprzcl2  12879  qmulz  12892  qre  12894  qnegcl  12907  elpqb  12917  xrmax1  13118  xrmin2  13121  max1ALT  13129  xlesubadd  13206  xmulass  13230  xlemul1a  13231  xrsupexmnf  13248  xrinfmexpnf  13249  xrub  13255  iccid  13334  fzsn  13511  fzsuc2  13527  fz1sbc  13545  elfzp12  13548  modmuladd  13866  seqid3  13999  bcval5  14271  bcpasc  14274  hashbnd  14289  hashnnn0genn0  14296  hashprg  14348  hashfzo  14382  tpfo  14453  wrdl1s1  14568  ccats1alpha  14573  cats1un  14674  s7f1o  14919  shftlem  15021  replim  15069  absmod0  15256  absz  15264  rlimdm  15504  summolem2  15669  summo  15670  zsum  15671  fsum  15673  fsummulc2  15737  fsumconst  15743  fsum00  15752  incexclem  15792  isumsplit  15796  infcvgaux1i  15813  prodmolem2  15891  prodmo  15892  zprod  15893  fprod  15897  prodsn  15918  prodsnf  15920  fprodconst  15934  ruclem2  16190  fzo0dvdseq  16283  bitsf1ocnv  16404  sadcaddlem  16417  smueqlem  16450  gcdabs1  16489  bezoutlem1  16499  bezoutlem3  16501  bezoutlem4  16502  dvdsgcd  16504  dvdsmulgcd  16516  lcmgcdeq  16572  lcmf  16593  lcmfunsnlem1  16597  lcmfunsnlem2lem2  16599  isprm2lem  16641  dvdsprime  16647  isprm5  16668  coprm  16672  prmdvdsexpr  16678  rpexp  16683  phibndlem  16731  dfphi2  16735  hashgcdlem  16749  odzdvds  16757  nnoddn2prm  16773  pythagtriplem1  16778  iserodd  16797  pceulem  16807  pcqmul  16815  pcqcl  16818  pcxnn0cl  16822  pcxcl  16823  pcneg  16836  pcabs  16837  pcgcd1  16839  pcz  16843  pcprmpw2  16844  pcprmpw  16845  dvdsprmpweqle  16848  difsqpwdvds  16849  pcaddlem  16850  pcadd  16851  pcmpt  16854  pockthg  16868  prmreclem5  16882  4sqlem4  16914  mul4sq  16916  vdwapun  16936  vdwlem2  16944  vdwlem6  16948  vdwlem8  16950  vdwlem13  16955  0ram  16982  ram0  16984  ramcl  16991  cshwsiun  17061  wunress  17210  firest  17386  isssc  17778  pospo  18300  latnlej  18413  gsumval2a  18644  xpsmnd0  18737  mnd1id  18739  0subm  18776  mulgnn0p1  19052  mulgnn0ass  19077  cyccom  19169  gicsubgen  19245  symg1bas  19357  snsymgefmndeq  19361  psgnunilem1  19459  psgnunilem2  19461  mndodcongi  19509  oddvdsnn0  19510  odnncl  19511  oddvds  19513  odeq  19516  odeq1  19526  pgpfi2  19572  sylow2a  19585  sylow2blem3  19588  sylow3lem6  19598  lsmelvalm  19617  lsmsubm  19619  lsmsubg  19620  lsmmod  19641  lsmdisj2  19648  efgmnvl  19680  efgtlen  19692  efgs1b  19702  efgrelexlemb  19716  efgredeu  19718  efgcpbllemb  19721  frgpuptinv  19737  frgpup3lem  19743  qusabl  19831  frgpnabllem1  19839  cyggeninv  19849  cyggenod  19850  gsumval3eu  19870  dprdssv  19984  dprdfeq0  19990  dprdsubg  19992  dprddisj2  20007  ablfacrp  20034  pgpfac1lem3  20045  pgpfaclem2  20050  xpsring1d  20304  dvreq1  20382  irredn1  20397  nzrunit  20496  ringcinv  20643  rrgeq0  20672  domneq0  20680  drngmul0orOLD  20733  isabvd  20784  abvdom  20802  issrngd  20827  lmodfopnelem2  20889  lss1d  20953  lspsneq0  21002  lbspss  21072  lsmcl  21073  lvecvs0or  21101  lspindpi  21125  lidl1el  21219  lpiss  21322  lidldvgen  21327  qsssubdrg  21401  zringlpirlem1  21437  pzriprnglem6  21461  pzriprnglem12  21467  znfld  21535  znunit  21538  znrrg  21540  cygznlem3  21544  frgpcyg  21548  psgnghm  21555  ipeq0  21613  cssincl  21663  lsmcss  21667  obselocv  21703  dsmmacl  21716  dsmmlss  21719  mplsubrglem  21978  mplmonmul  22012  mplcoe5lem  22015  mhpsclcl  22135  mhpvarcl  22136  psdmul  22154  coe1tmmul2  22262  coe1tmmul  22263  pf1ind  22341  mat1dimelbas  22454  mdetralt  22591  mdetunilem2  22596  mdetunilem7  22601  mdetunilem9  22603  maducoeval2  22623  chpscmat  22825  chfacfscmulgsum  22843  chfacfpmmulgsum  22847  istopon  22895  eltg3  22945  tgidm  22963  clsval2  23033  opncldf1  23067  restbas  23141  tgrest  23142  restcld  23155  restcldr  23157  restcls  23164  restntr  23165  ordtbas2  23174  ordtbas  23175  ordtrest2lem  23186  ordtrest2  23187  pnfnei  23203  mnfnei  23204  tgcn  23235  cnconst  23267  cnindis  23275  lmss  23281  ordtt1  23362  discmp  23381  1stcrest  23436  2ndcdisj  23439  cldllycmp  23478  txbas  23550  ptpjpre1  23554  ptuni2  23559  ptbasin  23560  ptbasfi  23564  ptopn2  23567  txbasval  23589  ptpjopn  23595  ptclsg  23598  dfac14lem  23600  xkoccn  23602  ptcnp  23605  upxp  23606  ptrescn  23622  txkgen  23635  xkoptsub  23637  xkopt  23638  xkoco1cn  23640  xkoco2cn  23641  xkococn  23643  xkoinjcn  23670  ordthmeolem  23784  ptuncnv  23790  nrmhaus  23809  fbssint  23821  fbfinnfr  23824  fbasrn  23867  isufil2  23891  filufint  23903  rnelfm  23936  fmfnfmlem2  23938  fmfnfmlem3  23939  fmfnfmlem4  23940  fmfnfm  23941  flimtopon  23953  flimclslem  23967  fclstopon  23995  fclscf  24008  flimfnfcls  24011  alexsublem  24027  alexsubALTlem3  24032  alexsubALTlem4  24033  ptcmplem2  24036  tmdgsum2  24079  symgtgp  24089  cldsubg  24094  qustgplem  24104  tgptsmscld  24134  tsmsxplem1  24136  imasdsf1olem  24356  blssps  24407  blss  24408  stdbdxmet  24498  methaus  24503  metrest  24507  nrginvrcn  24675  nmoeq0  24719  blssioo  24778  xrtgioo  24790  xrsxmet  24793  reconnlem1  24810  reconnlem2  24811  xrge0tsms  24818  elcncf1di  24880  iccpnfcnv  24929  evth  24944  lebnumlem1  24946  lebnumlem2  24947  lebnumlem3  24948  nmoleub3  25104  minveclem3b  25413  ivthlem2  25437  ivthlem3  25438  elovolm  25460  ovolmge0  25462  ovoliun  25490  ovolicc2lem3  25504  ovolicc2  25507  voliunlem3  25537  dyaddisj  25581  dyadmax  25583  opnmblALT  25588  ismbfd  25624  ismbf2d  25625  mbfimaopnlem  25640  mbfimaopn2  25642  i1fmullem  25679  i1fres  25690  itg1climres  25699  mbfi1fseqlem4  25703  itg2lcl  25712  itgsplitioo  25823  ellimc2  25862  rolle  25975  dvlip  25978  dvge0  25991  dvne0  25996  lhop1lem  25998  tdeglem4  26043  degltlem1  26055  deg1nn0clb  26073  deg1lt0  26074  dvdsq1p  26146  ply1rem  26149  fta1g  26153  elply2  26179  plyf  26181  ne0p  26190  plyeq0lem  26193  plypf1  26195  0dgrb  26229  coe1termlem  26241  dgrcolem2  26257  plymul0or  26265  plyrem  26289  fta1  26292  quotcan  26293  aalioulem3  26318  eff1olem  26530  lognegb  26572  eflogeq  26584  argregt0  26592  argrege0  26593  tanarg  26601  cxpexp  26650  cxpeq0  26660  mulcxp  26667  cxpeq  26739  atans2  26913  scvxcvx  26967  dmgmaddn0  27004  isppw2  27096  vmappw  27097  vmacl  27099  efvmacl  27101  isnsqf  27116  mumullem2  27161  sqff1o  27163  dvdsppwf1o  27167  ppiublem1  27183  vmalelog  27186  chtublem  27192  fsumvma  27194  perfectlem2  27211  perfect  27212  bposlem1  27265  lgsmod  27304  lgsne0  27316  lgsdirnn0  27325  lgsqr  27332  lgsdchr  27336  gausslemma2dlem1a  27346  gausslemma2dlem6  27353  lgseisenlem2  27357  lgsquadlem1  27361  lgsquadlem2  27362  2lgslem1b  27373  2sqlem2  27399  mul2sq  27400  2sqlem7  27405  dchrisum0fno1  27492  pntrsumbnd2  27548  ostthlem1  27608  ostth2lem2  27615  ostth3  27619  ostth  27620  nolesgn2ores  27654  nogesgn1ores  27656  nolt02o  27677  nogt01o  27678  nosupbnd2  27698  noinfbnd2lem1  27712  noetasuplem4  27718  noetainflem4  27722  maxs1  27751  mins2  27754  ltsne  27756  eqcuts3  27814  cuteq1  27827  madef  27846  ltslpss  27918  lrrecfr  27953  addsval  27972  addsproplem2  27980  addsuniflem  28011  addbdaylem  28027  negsid  28051  negsunif  28065  mulsproplem5  28130  mulsproplem6  28131  mulsproplem7  28132  mulsproplem8  28133  mulsproplem9  28134  lemulsd  28148  sltmuls1  28157  sltmuls2  28158  ltmuls2  28181  muls0ord  28195  precsexlem8  28224  precsexlem9  28225  precsexlem11  28227  elons2  28268  oncutlt  28274  bdayons  28286  onaddscl  28287  onmulscl  28288  nnsge1  28353  n0fincut  28365  n0subs  28373  dfnns2  28382  eucliddivs  28386  znegscl  28402  zaddscl  28404  zmulscld  28407  elzn0s  28408  eln0zs  28410  n0seo  28431  zseo  28432  bdaypw2n0bndlem  28473  bdaypw2n0bnd  28474  z12no  28486  z12addscl  28487  z12negscl  28488  z12shalf  28490  z12zsodd  28492  z12sge0  28493  z12bdaylem  28494  bdayfinlem  28496  recut  28504  elreno2  28505  remulscllem1  28510  colinearalg  28997  axpasch  29028  axlowdimlem16  29044  axlowdimlem17  29045  axlowdim  29048  axcontlem2  29052  axcontlem4  29054  axcontlem7  29057  lpvtx  29155  edglnl  29230  numedglnl  29231  usgredgop  29257  usgrexmplef  29346  uhgrspansubgrlem  29377  uhgrspan1  29390  nbusgredgeu0  29455  nb3grprlem2  29468  cusgrsize2inds  29540  vtxd0nedgb  29575  rusgrpropnb  29670  upgrwlkvtxedg  29731  wlkp1lem1  29758  wlkp1lem6  29763  wlkp1lem8  29765  usgr2wlkneq  29842  crctcshwlk  29908  crctcsh  29910  iswwlksnon  29939  wlkiswwlks1  29953  wwlksnextbi  29980  wwlksnextproplem2  29996  wspthsnonn0vne  30003  clwlkclwwlklem2  30088  clwwisshclwws  30103  erclwwlktr  30110  clwwlkel  30134  clwwlkext2edg  30144  erclwwlkntr  30159  clwlknf1oclwwlknlem2  30170  clwlknf1oclwwlknlem3  30171  clwlknf1oclwwlkn  30172  clwwlknonccat  30184  0wlkons1  30209  3wlkdlem6  30253  eupth2eucrct  30305  frgrwopreglem2  30401  2clwwlk2clwwlk  30438  wlkl0  30455  nvmul0or  30739  ipasslem5  30924  ipasslem11  30929  hvmul0or  31114  his6  31188  hhssnv  31353  ocsh  31372  ocin  31385  shsidmi  31473  chnlen0  31533  h1de2bi  31643  h1de2ctlem  31644  h1de2ci  31645  spansni  31646  3oalem1  31751  nmcexi  32115  atcveq0  32437  chcv1  32444  cdjreui  32521  cdj3lem2b  32526  xrge0tsmsd  33154  1fldgenq  33406  psrmonmul  33734  ccfldextdgrr  33856  ordtrest2NEWlem  34106  ordtrest2NEW  34107  xrge0iifcnv  34117  esumc  34235  esumpcvgval  34262  ballotlemfc0  34677  ballotlemfcc  34678  fissorduni  35271  axprALT2  35290  fineqvnttrclse  35305  gblacfnacd  35330  subfacp1lem4  35411  subfacp1lem5  35412  erdszelem8  35426  sconnpi1  35467  cvmsss2  35502  cvmlift2lem12  35542  satfv0  35586  satfv0fun  35599  satf00  35602  sat1el2xp  35607  fmla0xp  35611  fmlasucdisj  35627  satffunlem1lem1  35630  satffunlem2lem1  35632  dmopab3rexdif  35633  msubco  35759  msubvrs  35788  ellcsrspsn  35869  sinccvglem  35900  untsucf  35938  nnuni  35955  dfrdg2  36021  colineardim1  36289  btwnconn1lem14  36328  segleantisym  36343  colinbtwnle  36346  outsidele  36360  lineunray  36375  linethru  36381  elicc3  36545  opnregcld  36558  cldregopn  36559  fnejoin2  36597  bj-isrvec  37654  dissneqlem  37702  icorempo  37713  relowlssretop  37725  relowlpssretop  37726  rdgssun  37740  finxpsuclem  37759  lindsenlbs  37982  ptrecube  37987  poimirlem6  37993  poimirlem7  37994  poimirlem16  38003  poimirlem17  38004  poimirlem19  38006  poimirlem20  38007  poimirlem21  38008  poimirlem22  38009  poimirlem23  38010  poimirlem24  38011  poimirlem25  38012  poimirlem26  38013  poimirlem27  38014  poimirlem29  38016  poimirlem30  38017  poimirlem31  38018  poimirlem32  38019  itg2addnclem3  38040  ftc1anclem6  38065  dvasin  38071  unirep  38081  sdclem2  38109  ssbnd  38155  prdsbnd  38160  cntotbnd  38163  heibor1lem  38176  rrnequiv  38202  ismndo2  38241  grpoeqdivid  38248  isdrngo3  38326  crngohomfo  38373  0idl  38392  1idl  38393  divrngidl  38395  smprngopr  38419  prnc  38434  ispridlc  38437  disjimeceqim  39171  riotaclbgBAD  39446  lshpdisj  39479  lsateln0  39487  lsatcveq0  39524  opnlen0  39680  cmtbr4N  39747  cvrnbtwn2  39767  cvrnbtwn4  39771  atcvreq0  39806  cvlatexch1  39828  exatleN  39896  atlelt  39930  ps-2  39970  llnn0  40008  lplnn0N  40039  islpln2a  40040  lvoln0N  40083  islvol2aN  40084  4at  40105  dalemcea  40152  dalem3  40156  pmapglb2N  40263  pmapglb2xN  40264  cdlema1N  40283  cdlemb  40286  paddasslem17  40328  llnexchb2lem  40360  llnexchb2  40361  lhpat3  40538  ltrnid  40627  trlne  40677  cdlemc4  40686  cdleme11h  40758  cdlemednuN  40792  cdlemg1a  41062  tendoeq2  41266  tendoid0  41317  dva1dim  41477  dib1dim  41657  dihlatat  41829  dochkrshp4  41881  dochkr1  41970  lclkrlem2e  42003  lcfrlem16  42050  lcfrlem28  42062  mapd0  42157  hdmap14lem13  42372  eqresfnbd  42719  expeq1d  42801  expeqidd  42802  dvdsexpnn0  42811  reladdrsub  42862  sn-remul0ord  42885  sn-negex12  42894  sn-mullid  42913  sn-mul02  42942  nn0addcom  42952  nn0mulcom  42956  zmulcomlem  42957  mulgt0con1d  42960  mulgt0con2d  42961  sn-sup2  42981  frlmsnic  43026  evlselvlem  43038  prjspner1  43076  elrfi  43143  mrefg2  43156  eldiophb  43206  eldioph2b  43212  diophin  43221  diophun  43222  rexzrexnn0  43249  eldioph4b  43256  diophren  43258  rencldnfilem  43265  pellexlem6  43279  jm2.19  43438  rmydioph  43459  expdiophlem1  43466  expdioph  43468  lnr2i  43561  lpirlnr  43562  hbtlem2  43569  hbtlem4  43571  hbtlem6  43574  dgrsub2  43580  dgraa0p  43594  rngunsnply  43614  nlimsuc  43885  dfsucon  43967  radcnvrat  44758  pm14.24  44876  addrcom  44918  modelaxreplem1  45422  ormklocald  47319  natlocalincr  47321  afveu  47616  dfafn5b  47624  rlimdmafv  47640  afv2eu  47701  rlimdmafv2  47721  el1fzopredsuc  47789  minusmod5ne  47818  modmknepk  47831  elsetpreimafvssdm  47861  imasetpreimafvbijlemfo  47880  sprvalpw  47955  prprvalpw  47990  reupr  47997  fmtnofac2lem  48046  proththdlem  48091  perfectALTVlem2  48213  perfectALTV  48214  gbowpos  48250  gbowgt5  48253  gboge9  48255  nnsum4primesodd  48287  nnsum4primesoddALTV  48288  uhgrimedgi  48381  isuspgrim0  48385  isuspgrimlem  48386  upgrimpths  48400  clnbgrgrim  48425  grimedg  48426  grtrissvtx  48435  stgredgiun  48449  stgrvtx0  48453  isubgr3stgrlem7  48463  grlimgrtrilem2  48493  gpgiedgdmellem  48537  gpgvtxel2  48539  gpgvtx0  48544  gpgvtx1  48545  gpgusgralem  48547  gpgedgvtx0  48552  gpgedgvtx1  48553  gpgedg2ov  48557  gpgedg2iv  48558  gpgnbgrvtx0  48565  gpgnbgrvtx1  48566  pgnbgreunbgr  48616  ringcinvALTV  48801  lincellss  48917  lindsrng01  48959  suppdm  49001  nnpw2pb  49078  0aryfvalel  49125  0aryfvalelfv  49126  itsclc0xyqsolr  49260  infsubc  49550  infsubc2  49551