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  4489  elsn2g  4618  preq1b  4799  elpreqprb  4821  reusv3  5347  alxfr  5349  reuhypd  5361  axpr  5369  opth1  5420  euotd  5458  otiunsndisj  5465  tz7.2  5604  frsn  5709  dmopab2rex  5863  elsnxp  6246  reuop  6248  dfpo2  6251  ordtri1  6347  ordtri3  6350  fvmptdv2  6956  fveqressseq  7021  foco2  7051  fsn  7077  fnsnbg  7107  fnsnbOLD  7109  fmptsng  7111  fmptsnd  7112  fconst2g  7146  fnprb  7151  fntpb  7152  funfvima  7173  soisoi  7271  isores3  7278  eqfunresadj  7303  riotaeqimp  7338  eusvobj2  7347  ovmpodv2  7513  f1opw2  7610  sorpssun  7672  sorpssin  7673  oneqmin  7742  nlimsucg  7781  onzsl  7785  tfinds  7799  funcnvuni  7871  mptcnfimad  7927  opiota  8000  mposn  8042  frpoins3xpg  8079  frpoins3xp3g  8080  poxp2  8082  xpord2pred  8084  sexp2  8085  poxp3  8089  xpord3pred  8091  sexp3  8092  xpord3inddlem  8093  suppssov1  8136  suppssov2  8137  suppssfv  8141  brtpos  8174  frrlem12  8236  frrlem13  8237  seqomlem1  8378  seqomlem2  8379  omordi  8490  omord  8492  omwordi  8495  oeeui  8526  nnmordi  8555  nnmord  8556  nnmwordi  8559  nnawordex  8561  nnaordex  8562  nneob  8580  omsmolem  8581  eldifsucnn  8588  qsss  8709  eroveu  8745  mapsncnv  8827  ralxpmap  8830  elixpsn  8871  ixpsnf1o  8872  boxcutc  8875  pw2f1olem  9005  2pwne  9057  mapxpen  9067  mapunen  9070  php  9127  onomeneq  9134  unxpdomlem2  9152  en1eqsnbi  9171  isfiniteg  9195  fofinf1o  9227  f1opwfi  9251  elfiun  9325  oieu  9436  brwdom2  9470  wdomtr  9472  ixpiunwdom  9487  en3lplem1  9513  suc11reg  9520  inf3lemd  9528  cantnfvalf  9566  cantnflt  9573  cantnfp1lem3  9581  cantnflem2  9591  ttrcltr  9617  rnttrcl  9623  ttrclselem1  9626  r1tr  9680  updjud  9838  dfac8alem  9931  wdomnumr  9966  isinfcard  9994  aceq3lem  10022  dfac5lem4  10028  dfac5lem4OLD  10030  dfac5  10031  dfac2b  10033  coftr  10175  fin23lem28  10242  fin23lem29  10243  fin1a2lem11  10312  fin1a2lem12  10313  fin1a2lem13  10314  hsmexlem9  10327  axdclem  10421  pwcfsdom  10485  gchdomtri  10531  fpwwe2  10545  gchpwdom  10572  gchhar  10581  addnidpi  10803  nqereu  10831  genpv  10901  genpdm  10904  distrlem5pr  10929  mulrid  11121  ltne  11221  mul02  11302  cnegex  11305  mul0or  11768  negfi  12082  sup2  12089  supaddc  12100  supadd  12101  supmul1  12102  supmul  12105  creur  12130  creui  12131  cju  12132  nnsub  12180  un0addcl  12425  un0mulcl  12426  nn0sub  12442  elz2  12497  zaddcl  12522  suprzcl2  12842  qmulz  12855  qre  12857  qnegcl  12870  elpqb  12880  xrmax1  13081  xrmin2  13084  max1ALT  13092  xlesubadd  13169  xmulass  13193  xlemul1a  13194  xrsupexmnf  13211  xrinfmexpnf  13212  xrub  13218  iccid  13297  fzsn  13473  fzsuc2  13489  fz1sbc  13507  elfzp12  13510  modmuladd  13827  seqid3  13960  bcval5  14232  bcpasc  14235  hashbnd  14250  hashnnn0genn0  14257  hashprg  14309  hashfzo  14343  tpfo  14414  wrdl1s1  14529  ccats1alpha  14534  cats1un  14635  s7f1o  14880  shftlem  14982  replim  15030  absmod0  15217  absz  15225  rlimdm  15465  summolem2  15630  summo  15631  zsum  15632  fsum  15634  fsummulc2  15698  fsumconst  15704  fsum00  15712  incexclem  15750  isumsplit  15754  infcvgaux1i  15771  prodmolem2  15849  prodmo  15850  zprod  15851  fprod  15855  prodsn  15876  prodsnf  15878  fprodconst  15892  ruclem2  16148  fzo0dvdseq  16241  bitsf1ocnv  16362  sadcaddlem  16375  smueqlem  16408  gcdabs1  16447  bezoutlem1  16457  bezoutlem3  16459  bezoutlem4  16460  dvdsgcd  16462  dvdsmulgcd  16474  lcmgcdeq  16530  lcmf  16551  lcmfunsnlem1  16555  lcmfunsnlem2lem2  16557  isprm2lem  16599  dvdsprime  16605  isprm5  16625  coprm  16629  prmdvdsexpr  16635  rpexp  16640  phibndlem  16688  dfphi2  16692  hashgcdlem  16706  odzdvds  16714  nnoddn2prm  16730  pythagtriplem1  16735  iserodd  16754  pceulem  16764  pcqmul  16772  pcqcl  16775  pcxnn0cl  16779  pcxcl  16780  pcneg  16793  pcabs  16794  pcgcd1  16796  pcz  16800  pcprmpw2  16801  pcprmpw  16802  dvdsprmpweqle  16805  difsqpwdvds  16806  pcaddlem  16807  pcadd  16808  pcmpt  16811  pockthg  16825  prmreclem5  16839  4sqlem4  16871  mul4sq  16873  vdwapun  16893  vdwlem2  16901  vdwlem6  16905  vdwlem8  16907  vdwlem13  16912  0ram  16939  ram0  16941  ramcl  16948  cshwsiun  17018  wunress  17167  firest  17343  isssc  17735  pospo  18257  latnlej  18370  gsumval2a  18601  xpsmnd0  18694  mnd1id  18696  0subm  18733  mulgnn0p1  19006  mulgnn0ass  19031  cyccom  19123  gicsubgen  19199  symg1bas  19311  snsymgefmndeq  19315  psgnunilem1  19413  psgnunilem2  19415  mndodcongi  19463  oddvdsnn0  19464  odnncl  19465  oddvds  19467  odeq  19470  odeq1  19480  pgpfi2  19526  sylow2a  19539  sylow2blem3  19542  sylow3lem6  19552  lsmelvalm  19571  lsmsubm  19573  lsmsubg  19574  lsmmod  19595  lsmdisj2  19602  efgmnvl  19634  efgtlen  19646  efgs1b  19656  efgrelexlemb  19670  efgredeu  19672  efgcpbllemb  19675  frgpuptinv  19691  frgpup3lem  19697  qusabl  19785  frgpnabllem1  19793  cyggeninv  19803  cyggenod  19804  gsumval3eu  19824  dprdssv  19938  dprdfeq0  19944  dprdsubg  19946  dprddisj2  19961  ablfacrp  19988  pgpfac1lem3  19999  pgpfaclem2  20004  xpsring1d  20260  dvreq1  20338  irredn1  20353  nzrunit  20448  ringcinv  20595  rrgeq0  20624  domneq0  20632  drngmul0orOLD  20685  isabvd  20736  abvdom  20754  issrngd  20779  lmodfopnelem2  20841  lss1d  20905  lspsneq0  20954  lbspss  21025  lsmcl  21026  lvecvs0or  21054  lspindpi  21078  lidl1el  21172  lpiss  21275  lidldvgen  21280  qsssubdrg  21372  zringlpirlem1  21408  pzriprnglem6  21432  pzriprnglem12  21438  znfld  21506  znunit  21509  znrrg  21511  cygznlem3  21515  frgpcyg  21519  psgnghm  21526  ipeq0  21584  cssincl  21634  lsmcss  21638  obselocv  21674  dsmmacl  21687  dsmmlss  21690  mplsubrglem  21950  mplmonmul  21982  mplcoe5lem  21985  mhpsclcl  22081  mhpvarcl  22082  psdmul  22100  coe1tmmul2  22209  coe1tmmul  22210  pf1ind  22290  mat1dimelbas  22406  mdetralt  22543  mdetunilem2  22548  mdetunilem7  22553  mdetunilem9  22555  maducoeval2  22575  chpscmat  22777  chfacfscmulgsum  22795  chfacfpmmulgsum  22799  istopon  22847  eltg3  22897  tgidm  22915  clsval2  22985  opncldf1  23019  restbas  23093  tgrest  23094  restcld  23107  restcldr  23109  restcls  23116  restntr  23117  ordtbas2  23126  ordtbas  23127  ordtrest2lem  23138  ordtrest2  23139  pnfnei  23155  mnfnei  23156  tgcn  23187  cnconst  23219  cnindis  23227  lmss  23233  ordtt1  23314  discmp  23333  1stcrest  23388  2ndcdisj  23391  cldllycmp  23430  txbas  23502  ptpjpre1  23506  ptuni2  23511  ptbasin  23512  ptbasfi  23516  ptopn2  23519  txbasval  23541  ptpjopn  23547  ptclsg  23550  dfac14lem  23552  xkoccn  23554  ptcnp  23557  upxp  23558  ptrescn  23574  txkgen  23587  xkoptsub  23589  xkopt  23590  xkoco1cn  23592  xkoco2cn  23593  xkococn  23595  xkoinjcn  23622  ordthmeolem  23736  ptuncnv  23742  nrmhaus  23761  fbssint  23773  fbfinnfr  23776  fbasrn  23819  isufil2  23843  filufint  23855  rnelfm  23888  fmfnfmlem2  23890  fmfnfmlem3  23891  fmfnfmlem4  23892  fmfnfm  23893  flimtopon  23905  flimclslem  23919  fclstopon  23947  fclscf  23960  flimfnfcls  23963  alexsublem  23979  alexsubALTlem3  23984  alexsubALTlem4  23985  ptcmplem2  23988  tmdgsum2  24031  symgtgp  24041  cldsubg  24046  qustgplem  24056  tgptsmscld  24086  tsmsxplem1  24088  imasdsf1olem  24308  blssps  24359  blss  24360  stdbdxmet  24450  methaus  24455  metrest  24459  nrginvrcn  24627  nmoeq0  24671  blssioo  24730  xrtgioo  24742  xrsxmet  24745  reconnlem1  24762  reconnlem2  24763  xrge0tsms  24770  elcncf1di  24835  iccpnfcnv  24889  evth  24905  lebnumlem1  24907  lebnumlem2  24908  lebnumlem3  24909  nmoleub3  25066  minveclem3b  25375  ivthlem2  25400  ivthlem3  25401  elovolm  25423  ovolmge0  25425  ovoliun  25453  ovolicc2lem3  25467  ovolicc2  25470  voliunlem3  25500  dyaddisj  25544  dyadmax  25546  opnmblALT  25551  ismbfd  25587  ismbf2d  25588  mbfimaopnlem  25603  mbfimaopn2  25605  i1fmullem  25642  i1fres  25653  itg1climres  25662  mbfi1fseqlem4  25666  itg2lcl  25675  itgsplitioo  25786  ellimc2  25825  rolle  25941  dvlip  25945  dvge0  25958  dvne0  25963  lhop1lem  25965  tdeglem4  26012  degltlem1  26024  deg1nn0clb  26042  deg1lt0  26043  dvdsq1p  26115  ply1rem  26118  fta1g  26122  elply2  26148  plyf  26150  ne0p  26159  plyeq0lem  26162  plypf1  26164  0dgrb  26198  coe1termlem  26210  dgrcolem2  26227  plymul0or  26235  plyrem  26260  fta1  26263  quotcan  26264  aalioulem3  26289  eff1olem  26504  lognegb  26546  eflogeq  26558  argregt0  26566  argrege0  26567  tanarg  26575  cxpexp  26624  cxpeq0  26634  mulcxp  26641  cxpeq  26714  atans2  26888  scvxcvx  26943  dmgmaddn0  26980  isppw2  27072  vmappw  27073  vmacl  27075  efvmacl  27077  isnsqf  27092  mumullem2  27137  sqff1o  27139  dvdsppwf1o  27143  ppiublem1  27160  vmalelog  27163  chtublem  27169  fsumvma  27171  perfectlem2  27188  perfect  27189  bposlem1  27242  lgsmod  27281  lgsne0  27293  lgsdirnn0  27302  lgsqr  27309  lgsdchr  27313  gausslemma2dlem1a  27323  gausslemma2dlem6  27330  lgseisenlem2  27334  lgsquadlem1  27338  lgsquadlem2  27339  2lgslem1b  27350  2sqlem2  27376  mul2sq  27377  2sqlem7  27382  dchrisum0fno1  27469  pntrsumbnd2  27525  ostthlem1  27585  ostth2lem2  27592  ostth3  27596  ostth  27597  nolesgn2ores  27631  nogesgn1ores  27633  nolt02o  27654  nogt01o  27655  nosupbnd2  27675  noinfbnd2lem1  27689  noetasuplem4  27695  noetainflem4  27699  maxs1  27724  mins2  27727  sltne  27729  eqscut3  27785  cuteq1  27798  madef  27817  sltlpss  27873  lrrecfr  27906  addsval  27925  addsproplem2  27933  addsuniflem  27964  addsbdaylem  27979  negsid  28003  negsunif  28017  mulsproplem5  28079  mulsproplem6  28080  mulsproplem7  28081  mulsproplem8  28082  mulsproplem9  28083  slemuld  28097  ssltmul1  28106  ssltmul2  28107  sltmul2  28130  muls0ord  28144  precsexlem8  28172  precsexlem9  28173  precsexlem11  28175  elons2  28215  onscutlt  28221  bdayon  28229  onaddscl  28230  onmulscl  28231  nnsge1  28291  n0sfincut  28302  n0subs  28309  dfnns2  28317  eucliddivs  28321  znegscl  28336  zaddscl  28338  zmulscld  28341  elzn0s  28342  eln0zs  28344  n0seo  28364  zseo  28365  zs12no  28406  zs12addscl  28407  zs12negscl  28408  zs12half  28410  zs12zodd  28412  zs12ge0  28413  zs12bday  28414  recut  28418  0reno  28419  remulscllem1  28422  colinearalg  28909  axpasch  28940  axlowdimlem16  28956  axlowdimlem17  28957  axlowdim  28960  axcontlem2  28964  axcontlem4  28966  axcontlem7  28969  lpvtx  29067  edglnl  29142  numedglnl  29143  usgredgop  29169  usgrexmplef  29258  uhgrspansubgrlem  29289  uhgrspan1  29302  nbusgredgeu0  29367  nb3grprlem2  29380  cusgrsize2inds  29453  vtxd0nedgb  29488  rusgrpropnb  29583  upgrwlkvtxedg  29644  wlkp1lem1  29671  wlkp1lem6  29676  wlkp1lem8  29678  usgr2wlkneq  29755  crctcshwlk  29821  crctcsh  29823  iswwlksnon  29852  wlkiswwlks1  29866  wwlksnextbi  29893  wwlksnextproplem2  29909  wspthsnonn0vne  29916  clwlkclwwlklem2  30001  clwwisshclwws  30016  erclwwlktr  30023  clwwlkel  30047  clwwlkext2edg  30057  erclwwlkntr  30072  clwlknf1oclwwlknlem2  30083  clwlknf1oclwwlknlem3  30084  clwlknf1oclwwlkn  30085  clwwlknonccat  30097  0wlkons1  30122  3wlkdlem6  30166  eupth2eucrct  30218  frgrwopreglem2  30314  2clwwlk2clwwlk  30351  wlkl0  30368  nvmul0or  30651  ipasslem5  30836  ipasslem11  30841  hvmul0or  31026  his6  31100  hhssnv  31265  ocsh  31284  ocin  31297  shsidmi  31385  chnlen0  31445  h1de2bi  31555  h1de2ctlem  31556  h1de2ci  31557  spansni  31558  3oalem1  31663  nmcexi  32027  atcveq0  32349  chcv1  32356  cdjreui  32433  cdj3lem2b  32438  xrge0tsmsd  33083  1fldgenq  33332  ccfldextdgrr  33757  ordtrest2NEWlem  34007  ordtrest2NEW  34008  xrge0iifcnv  34018  esumc  34136  esumpcvgval  34163  ballotlemfc0  34578  ballotlemfcc  34579  fissorduni  35173  fineqvnttrclse  35216  gblacfnacd  35218  subfacp1lem4  35299  subfacp1lem5  35300  erdszelem8  35314  sconnpi1  35355  cvmsss2  35390  cvmlift2lem12  35430  satfv0  35474  satfv0fun  35487  satf00  35490  sat1el2xp  35495  fmla0xp  35499  fmlasucdisj  35515  satffunlem1lem1  35518  satffunlem2lem1  35520  dmopab3rexdif  35521  msubco  35647  msubvrs  35676  ellcsrspsn  35757  sinccvglem  35788  untsucf  35826  nnuni  35843  dfrdg2  35909  colineardim1  36177  btwnconn1lem14  36216  segleantisym  36231  colinbtwnle  36234  outsidele  36248  lineunray  36263  linethru  36269  elicc3  36433  opnregcld  36446  cldregopn  36447  fnejoin2  36485  bj-isrvec  37411  dissneqlem  37457  icorempo  37468  relowlssretop  37480  relowlpssretop  37481  rdgssun  37495  finxpsuclem  37514  lindsenlbs  37728  ptrecube  37733  poimirlem6  37739  poimirlem7  37740  poimirlem16  37749  poimirlem17  37750  poimirlem19  37752  poimirlem20  37753  poimirlem21  37754  poimirlem22  37755  poimirlem23  37756  poimirlem24  37757  poimirlem25  37758  poimirlem26  37759  poimirlem27  37760  poimirlem29  37762  poimirlem30  37763  poimirlem31  37764  poimirlem32  37765  itg2addnclem3  37786  ftc1anclem6  37811  dvasin  37817  unirep  37827  sdclem2  37855  ssbnd  37901  prdsbnd  37906  cntotbnd  37909  heibor1lem  37922  rrnequiv  37948  ismndo2  37987  grpoeqdivid  37994  isdrngo3  38072  crngohomfo  38119  0idl  38138  1idl  38139  divrngidl  38141  smprngopr  38165  prnc  38180  ispridlc  38183  riotaclbgBAD  39126  lshpdisj  39159  lsateln0  39167  lsatcveq0  39204  opnlen0  39360  cmtbr4N  39427  cvrnbtwn2  39447  cvrnbtwn4  39451  atcvreq0  39486  cvlatexch1  39508  exatleN  39576  atlelt  39610  ps-2  39650  llnn0  39688  lplnn0N  39719  islpln2a  39720  lvoln0N  39763  islvol2aN  39764  4at  39785  dalemcea  39832  dalem3  39836  pmapglb2N  39943  pmapglb2xN  39944  cdlema1N  39963  cdlemb  39966  paddasslem17  40008  llnexchb2lem  40040  llnexchb2  40041  lhpat3  40218  ltrnid  40307  trlne  40357  cdlemc4  40366  cdleme11h  40438  cdlemednuN  40472  cdlemg1a  40742  tendoeq2  40946  tendoid0  40997  dva1dim  41157  dib1dim  41337  dihlatat  41509  dochkrshp4  41561  dochkr1  41650  lclkrlem2e  41683  lcfrlem16  41730  lcfrlem28  41742  mapd0  41837  hdmap14lem13  42052  eqresfnbd  42403  f1o2d2  42404  expeq1d  42494  expeqidd  42495  dvdsexpnn0  42504  reladdrsub  42555  sn-remul0ord  42578  sn-negex12  42587  sn-mullid  42606  sn-mul02  42622  nn0addcom  42632  nn0mulcom  42636  zmulcomlem  42637  mulgt0con1d  42640  mulgt0con2d  42641  sn-sup2  42661  frlmsnic  42710  evlselvlem  42744  prjspner1  42784  elrfi  42851  mrefg2  42864  eldiophb  42914  eldioph2b  42920  diophin  42929  diophun  42930  rexzrexnn0  42961  eldioph4b  42968  diophren  42970  rencldnfilem  42977  pellexlem6  42991  jm2.19  43150  rmydioph  43171  expdiophlem1  43178  expdioph  43180  lnr2i  43273  lpirlnr  43274  hbtlem2  43281  hbtlem4  43283  hbtlem6  43286  dgrsub2  43292  dgraa0p  43306  rngunsnply  43326  nlimsuc  43598  dfsucon  43680  radcnvrat  44471  pm14.24  44589  addrcom  44631  modelaxreplem1  45135  ormklocald  47034  natlocalincr  47036  afveu  47315  dfafn5b  47323  rlimdmafv  47339  afv2eu  47400  rlimdmafv2  47420  el1fzopredsuc  47487  minusmod5ne  47511  modmknepk  47524  elsetpreimafvssdm  47548  imasetpreimafvbijlemfo  47567  sprvalpw  47642  prprvalpw  47677  reupr  47684  fmtnofac2lem  47730  proththdlem  47775  perfectALTVlem2  47884  perfectALTV  47885  gbowpos  47921  gbowgt5  47924  gboge9  47926  nnsum4primesodd  47958  nnsum4primesoddALTV  47959  uhgrimedgi  48052  isuspgrim0  48056  isuspgrimlem  48057  upgrimpths  48071  clnbgrgrim  48096  grimedg  48097  grtrissvtx  48106  stgredgiun  48120  stgrvtx0  48124  isubgr3stgrlem7  48134  grlimgrtrilem2  48164  gpgiedgdmellem  48208  gpgvtxel2  48210  gpgvtx0  48215  gpgvtx1  48216  gpgusgralem  48218  gpgedgvtx0  48223  gpgedgvtx1  48224  gpgedg2ov  48228  gpgedg2iv  48229  gpgnbgrvtx0  48236  gpgnbgrvtx1  48237  pgnbgreunbgr  48287  ringcinvALTV  48472  lincellss  48588  lindsrng01  48630  suppdm  48672  nnpw2pb  48749  0aryfvalel  48796  0aryfvalelfv  48797  itsclc0xyqsolr  48931  infsubc  49221  infsubc2  49222