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  4479  elsn2g  4608  preq1b  4789  elpreqprb  4811  reusv3  5347  alxfr  5349  reuhypd  5361  axpr  5369  opth1  5428  euotd  5467  otiunsndisj  5474  tz7.2  5614  frsn  5719  dmopab2rex  5872  elsnxp  6255  reuop  6257  dfpo2  6260  ordtri1  6356  ordtri3  6359  fvmptdv2  6966  fveqressseq  7031  foco2  7061  fsn  7088  fnsnbg  7119  fnsnbOLD  7121  fmptsng  7123  fmptsnd  7124  fconst2g  7158  fnprb  7163  fntpb  7164  funfvima  7185  soisoi  7283  isores3  7290  eqfunresadj  7315  riotaeqimp  7350  eusvobj2  7359  ovmpodv2  7525  f1opw2  7622  sorpssun  7684  sorpssin  7685  oneqmin  7754  nlimsucg  7793  onzsl  7797  tfinds  7811  funcnvuni  7883  mptcnfimad  7939  opiota  8012  mposn  8053  frpoins3xpg  8090  frpoins3xp3g  8091  poxp2  8093  xpord2pred  8095  sexp2  8096  poxp3  8100  xpord3pred  8102  sexp3  8103  xpord3inddlem  8104  suppssov1  8147  suppssov2  8148  suppssfv  8152  brtpos  8185  frrlem12  8247  frrlem13  8248  seqomlem1  8389  seqomlem2  8390  omordi  8501  omord  8503  omwordi  8506  oeeui  8538  nnmordi  8567  nnmord  8568  nnmwordi  8571  nnawordex  8573  nnaordex  8574  nneob  8592  omsmolem  8593  eldifsucnn  8600  qsss  8722  eroveu  8759  mapsncnv  8841  ralxpmap  8844  elixpsn  8885  ixpsnf1o  8886  boxcutc  8889  pw2f1olem  9019  2pwne  9071  mapxpen  9081  mapunen  9084  php  9141  onomeneq  9148  unxpdomlem2  9167  en1eqsnbi  9186  isfiniteg  9210  fofinf1o  9242  f1opwfi  9266  elfiun  9343  oieu  9454  brwdom2  9488  wdomtr  9490  ixpiunwdom  9505  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  11243  mul02  11324  cnegex  11327  mul0or  11790  negfi  12105  sup2  12112  supaddc  12123  supadd  12124  supmul1  12125  supmul  12128  creur  12153  creui  12154  cju  12155  nnsub  12221  un0addcl  12470  un0mulcl  12471  nn0sub  12487  elz2  12542  zaddcl  12567  suprzcl2  12888  qmulz  12901  qre  12903  qnegcl  12916  elpqb  12926  xrmax1  13127  xrmin2  13130  max1ALT  13138  xlesubadd  13215  xmulass  13239  xlemul1a  13240  xrsupexmnf  13257  xrinfmexpnf  13258  xrub  13264  iccid  13343  fzsn  13520  fzsuc2  13536  fz1sbc  13554  elfzp12  13557  modmuladd  13875  seqid3  14008  bcval5  14280  bcpasc  14283  hashbnd  14298  hashnnn0genn0  14305  hashprg  14357  hashfzo  14391  tpfo  14462  wrdl1s1  14577  ccats1alpha  14582  cats1un  14683  s7f1o  14928  shftlem  15030  replim  15078  absmod0  15265  absz  15273  rlimdm  15513  summolem2  15678  summo  15679  zsum  15680  fsum  15682  fsummulc2  15746  fsumconst  15752  fsum00  15761  incexclem  15801  isumsplit  15805  infcvgaux1i  15822  prodmolem2  15900  prodmo  15901  zprod  15902  fprod  15906  prodsn  15927  prodsnf  15929  fprodconst  15943  ruclem2  16199  fzo0dvdseq  16292  bitsf1ocnv  16413  sadcaddlem  16426  smueqlem  16459  gcdabs1  16498  bezoutlem1  16508  bezoutlem3  16510  bezoutlem4  16511  dvdsgcd  16513  dvdsmulgcd  16525  lcmgcdeq  16581  lcmf  16602  lcmfunsnlem1  16606  lcmfunsnlem2lem2  16608  isprm2lem  16650  dvdsprime  16656  isprm5  16677  coprm  16681  prmdvdsexpr  16687  rpexp  16692  phibndlem  16740  dfphi2  16744  hashgcdlem  16758  odzdvds  16766  nnoddn2prm  16782  pythagtriplem1  16787  iserodd  16806  pceulem  16816  pcqmul  16824  pcqcl  16827  pcxnn0cl  16831  pcxcl  16832  pcneg  16845  pcabs  16846  pcgcd1  16848  pcz  16852  pcprmpw2  16853  pcprmpw  16854  dvdsprmpweqle  16857  difsqpwdvds  16858  pcaddlem  16859  pcadd  16860  pcmpt  16863  pockthg  16877  prmreclem5  16891  4sqlem4  16923  mul4sq  16925  vdwapun  16945  vdwlem2  16953  vdwlem6  16957  vdwlem8  16959  vdwlem13  16964  0ram  16991  ram0  16993  ramcl  17000  cshwsiun  17070  wunress  17219  firest  17395  isssc  17787  pospo  18309  latnlej  18422  gsumval2a  18653  xpsmnd0  18746  mnd1id  18748  0subm  18785  mulgnn0p1  19061  mulgnn0ass  19086  cyccom  19178  gicsubgen  19254  symg1bas  19366  snsymgefmndeq  19370  psgnunilem1  19468  psgnunilem2  19470  mndodcongi  19518  oddvdsnn0  19519  odnncl  19520  oddvds  19522  odeq  19525  odeq1  19535  pgpfi2  19581  sylow2a  19594  sylow2blem3  19597  sylow3lem6  19607  lsmelvalm  19626  lsmsubm  19628  lsmsubg  19629  lsmmod  19650  lsmdisj2  19657  efgmnvl  19689  efgtlen  19701  efgs1b  19711  efgrelexlemb  19725  efgredeu  19727  efgcpbllemb  19730  frgpuptinv  19746  frgpup3lem  19752  qusabl  19840  frgpnabllem1  19848  cyggeninv  19858  cyggenod  19859  gsumval3eu  19879  dprdssv  19993  dprdfeq0  19999  dprdsubg  20001  dprddisj2  20016  ablfacrp  20043  pgpfac1lem3  20054  pgpfaclem2  20059  xpsring1d  20313  dvreq1  20391  irredn1  20406  nzrunit  20501  ringcinv  20648  rrgeq0  20677  domneq0  20685  drngmul0orOLD  20738  isabvd  20789  abvdom  20807  issrngd  20832  lmodfopnelem2  20894  lss1d  20958  lspsneq0  21007  lbspss  21077  lsmcl  21078  lvecvs0or  21106  lspindpi  21130  lidl1el  21224  lpiss  21327  lidldvgen  21332  qsssubdrg  21406  zringlpirlem1  21442  pzriprnglem6  21466  pzriprnglem12  21472  znfld  21540  znunit  21543  znrrg  21545  cygznlem3  21549  frgpcyg  21553  psgnghm  21560  ipeq0  21618  cssincl  21668  lsmcss  21672  obselocv  21708  dsmmacl  21721  dsmmlss  21724  mplsubrglem  21982  mplmonmul  22014  mplcoe5lem  22017  mhpsclcl  22113  mhpvarcl  22114  psdmul  22132  coe1tmmul2  22241  coe1tmmul  22242  pf1ind  22320  mat1dimelbas  22436  mdetralt  22573  mdetunilem2  22578  mdetunilem7  22583  mdetunilem9  22585  maducoeval2  22605  chpscmat  22807  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  istopon  22877  eltg3  22927  tgidm  22945  clsval2  23015  opncldf1  23049  restbas  23123  tgrest  23124  restcld  23137  restcldr  23139  restcls  23146  restntr  23147  ordtbas2  23156  ordtbas  23157  ordtrest2lem  23168  ordtrest2  23169  pnfnei  23185  mnfnei  23186  tgcn  23217  cnconst  23249  cnindis  23257  lmss  23263  ordtt1  23344  discmp  23363  1stcrest  23418  2ndcdisj  23421  cldllycmp  23460  txbas  23532  ptpjpre1  23536  ptuni2  23541  ptbasin  23542  ptbasfi  23546  ptopn2  23549  txbasval  23571  ptpjopn  23577  ptclsg  23580  dfac14lem  23582  xkoccn  23584  ptcnp  23587  upxp  23588  ptrescn  23604  txkgen  23617  xkoptsub  23619  xkopt  23620  xkoco1cn  23622  xkoco2cn  23623  xkococn  23625  xkoinjcn  23652  ordthmeolem  23766  ptuncnv  23772  nrmhaus  23791  fbssint  23803  fbfinnfr  23806  fbasrn  23849  isufil2  23873  filufint  23885  rnelfm  23918  fmfnfmlem2  23920  fmfnfmlem3  23921  fmfnfmlem4  23922  fmfnfm  23923  flimtopon  23935  flimclslem  23949  fclstopon  23977  fclscf  23990  flimfnfcls  23993  alexsublem  24009  alexsubALTlem3  24014  alexsubALTlem4  24015  ptcmplem2  24018  tmdgsum2  24061  symgtgp  24071  cldsubg  24076  qustgplem  24086  tgptsmscld  24116  tsmsxplem1  24118  imasdsf1olem  24338  blssps  24389  blss  24390  stdbdxmet  24480  methaus  24485  metrest  24489  nrginvrcn  24657  nmoeq0  24701  blssioo  24760  xrtgioo  24772  xrsxmet  24775  reconnlem1  24792  reconnlem2  24793  xrge0tsms  24800  elcncf1di  24862  iccpnfcnv  24911  evth  24926  lebnumlem1  24928  lebnumlem2  24929  lebnumlem3  24930  nmoleub3  25086  minveclem3b  25395  ivthlem2  25419  ivthlem3  25420  elovolm  25442  ovolmge0  25444  ovoliun  25472  ovolicc2lem3  25486  ovolicc2  25489  voliunlem3  25519  dyaddisj  25563  dyadmax  25565  opnmblALT  25570  ismbfd  25606  ismbf2d  25607  mbfimaopnlem  25622  mbfimaopn2  25624  i1fmullem  25661  i1fres  25672  itg1climres  25681  mbfi1fseqlem4  25685  itg2lcl  25694  itgsplitioo  25805  ellimc2  25844  rolle  25957  dvlip  25960  dvge0  25973  dvne0  25978  lhop1lem  25980  tdeglem4  26025  degltlem1  26037  deg1nn0clb  26055  deg1lt0  26056  dvdsq1p  26128  ply1rem  26131  fta1g  26135  elply2  26161  plyf  26163  ne0p  26172  plyeq0lem  26175  plypf1  26177  0dgrb  26211  coe1termlem  26223  dgrcolem2  26239  plymul0or  26247  plyrem  26271  fta1  26274  quotcan  26275  aalioulem3  26300  eff1olem  26512  lognegb  26554  eflogeq  26566  argregt0  26574  argrege0  26575  tanarg  26583  cxpexp  26632  cxpeq0  26642  mulcxp  26649  cxpeq  26721  atans2  26895  scvxcvx  26949  dmgmaddn0  26986  isppw2  27078  vmappw  27079  vmacl  27081  efvmacl  27083  isnsqf  27098  mumullem2  27143  sqff1o  27145  dvdsppwf1o  27149  ppiublem1  27165  vmalelog  27168  chtublem  27174  fsumvma  27176  perfectlem2  27193  perfect  27194  bposlem1  27247  lgsmod  27286  lgsne0  27298  lgsdirnn0  27307  lgsqr  27314  lgsdchr  27318  gausslemma2dlem1a  27328  gausslemma2dlem6  27335  lgseisenlem2  27339  lgsquadlem1  27343  lgsquadlem2  27344  2lgslem1b  27355  2sqlem2  27381  mul2sq  27382  2sqlem7  27387  dchrisum0fno1  27474  pntrsumbnd2  27530  ostthlem1  27590  ostth2lem2  27597  ostth3  27601  ostth  27602  nolesgn2ores  27636  nogesgn1ores  27638  nolt02o  27659  nogt01o  27660  nosupbnd2  27680  noinfbnd2lem1  27694  noetasuplem4  27700  noetainflem4  27704  maxs1  27733  mins2  27736  ltsne  27738  eqcuts3  27796  cuteq1  27809  madef  27828  ltslpss  27900  lrrecfr  27935  addsval  27954  addsproplem2  27962  addsuniflem  27993  addbdaylem  28009  negsid  28033  negsunif  28047  mulsproplem5  28112  mulsproplem6  28113  mulsproplem7  28114  mulsproplem8  28115  mulsproplem9  28116  lemulsd  28130  sltmuls1  28139  sltmuls2  28140  ltmuls2  28163  muls0ord  28177  precsexlem8  28206  precsexlem9  28207  precsexlem11  28209  elons2  28250  oncutlt  28256  bdayons  28268  onaddscl  28269  onmulscl  28270  nnsge1  28335  n0fincut  28347  n0subs  28355  dfnns2  28364  eucliddivs  28368  znegscl  28384  zaddscl  28386  zmulscld  28389  elzn0s  28390  eln0zs  28392  n0seo  28413  zseo  28414  bdaypw2n0bndlem  28455  bdaypw2n0bnd  28456  z12no  28468  z12addscl  28469  z12negscl  28470  z12shalf  28472  z12zsodd  28474  z12sge0  28475  z12bdaylem  28476  bdayfinlem  28478  recut  28486  elreno2  28487  remulscllem1  28492  colinearalg  28979  axpasch  29010  axlowdimlem16  29026  axlowdimlem17  29027  axlowdim  29030  axcontlem2  29034  axcontlem4  29036  axcontlem7  29039  lpvtx  29137  edglnl  29212  numedglnl  29213  usgredgop  29239  usgrexmplef  29328  uhgrspansubgrlem  29359  uhgrspan1  29372  nbusgredgeu0  29437  nb3grprlem2  29450  cusgrsize2inds  29522  vtxd0nedgb  29557  rusgrpropnb  29652  upgrwlkvtxedg  29713  wlkp1lem1  29740  wlkp1lem6  29745  wlkp1lem8  29747  usgr2wlkneq  29824  crctcshwlk  29890  crctcsh  29892  iswwlksnon  29921  wlkiswwlks1  29935  wwlksnextbi  29962  wwlksnextproplem2  29978  wspthsnonn0vne  29985  clwlkclwwlklem2  30070  clwwisshclwws  30085  erclwwlktr  30092  clwwlkel  30116  clwwlkext2edg  30126  erclwwlkntr  30141  clwlknf1oclwwlknlem2  30152  clwlknf1oclwwlknlem3  30153  clwlknf1oclwwlkn  30154  clwwlknonccat  30166  0wlkons1  30191  3wlkdlem6  30235  eupth2eucrct  30287  frgrwopreglem2  30383  2clwwlk2clwwlk  30420  wlkl0  30437  nvmul0or  30721  ipasslem5  30906  ipasslem11  30911  hvmul0or  31096  his6  31170  hhssnv  31335  ocsh  31354  ocin  31367  shsidmi  31455  chnlen0  31515  h1de2bi  31625  h1de2ctlem  31626  h1de2ci  31627  spansni  31628  3oalem1  31733  nmcexi  32097  atcveq0  32419  chcv1  32426  cdjreui  32503  cdj3lem2b  32508  xrge0tsmsd  33134  1fldgenq  33383  psrmonmul  33694  ccfldextdgrr  33816  ordtrest2NEWlem  34066  ordtrest2NEW  34067  xrge0iifcnv  34077  esumc  34195  esumpcvgval  34222  ballotlemfc0  34637  ballotlemfcc  34638  fissorduni  35233  axprALT2  35253  fineqvnttrclse  35268  gblacfnacd  35284  subfacp1lem4  35365  subfacp1lem5  35366  erdszelem8  35380  sconnpi1  35421  cvmsss2  35456  cvmlift2lem12  35496  satfv0  35540  satfv0fun  35553  satf00  35556  sat1el2xp  35561  fmla0xp  35565  fmlasucdisj  35581  satffunlem1lem1  35584  satffunlem2lem1  35586  dmopab3rexdif  35587  msubco  35713  msubvrs  35742  ellcsrspsn  35823  sinccvglem  35854  untsucf  35892  nnuni  35909  dfrdg2  35975  colineardim1  36243  btwnconn1lem14  36282  segleantisym  36297  colinbtwnle  36300  outsidele  36314  lineunray  36329  linethru  36335  elicc3  36499  opnregcld  36512  cldregopn  36513  fnejoin2  36551  bj-isrvec  37608  dissneqlem  37656  icorempo  37667  relowlssretop  37679  relowlpssretop  37680  rdgssun  37694  finxpsuclem  37713  lindsenlbs  37936  ptrecube  37941  poimirlem6  37947  poimirlem7  37948  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  poimirlem23  37964  poimirlem24  37965  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  poimirlem29  37970  poimirlem30  37971  poimirlem31  37972  poimirlem32  37973  itg2addnclem3  37994  ftc1anclem6  38019  dvasin  38025  unirep  38035  sdclem2  38063  ssbnd  38109  prdsbnd  38114  cntotbnd  38117  heibor1lem  38130  rrnequiv  38156  ismndo2  38195  grpoeqdivid  38202  isdrngo3  38280  crngohomfo  38327  0idl  38346  1idl  38347  divrngidl  38349  smprngopr  38373  prnc  38388  ispridlc  38391  disjimeceqim  39125  riotaclbgBAD  39400  lshpdisj  39433  lsateln0  39441  lsatcveq0  39478  opnlen0  39634  cmtbr4N  39701  cvrnbtwn2  39721  cvrnbtwn4  39725  atcvreq0  39760  cvlatexch1  39782  exatleN  39850  atlelt  39884  ps-2  39924  llnn0  39962  lplnn0N  39993  islpln2a  39994  lvoln0N  40037  islvol2aN  40038  4at  40059  dalemcea  40106  dalem3  40110  pmapglb2N  40217  pmapglb2xN  40218  cdlema1N  40237  cdlemb  40240  paddasslem17  40282  llnexchb2lem  40314  llnexchb2  40315  lhpat3  40492  ltrnid  40581  trlne  40631  cdlemc4  40640  cdleme11h  40712  cdlemednuN  40746  cdlemg1a  41016  tendoeq2  41220  tendoid0  41271  dva1dim  41431  dib1dim  41611  dihlatat  41783  dochkrshp4  41835  dochkr1  41924  lclkrlem2e  41957  lcfrlem16  42004  lcfrlem28  42016  mapd0  42111  hdmap14lem13  42326  eqresfnbd  42673  f1o2d2  42674  expeq1d  42756  expeqidd  42757  dvdsexpnn0  42766  reladdrsub  42817  sn-remul0ord  42840  sn-negex12  42849  sn-mullid  42868  sn-mul02  42897  nn0addcom  42907  nn0mulcom  42911  zmulcomlem  42912  mulgt0con1d  42915  mulgt0con2d  42916  sn-sup2  42936  frlmsnic  42985  evlselvlem  43019  prjspner1  43059  elrfi  43126  mrefg2  43139  eldiophb  43189  eldioph2b  43195  diophin  43204  diophun  43205  rexzrexnn0  43232  eldioph4b  43239  diophren  43241  rencldnfilem  43248  pellexlem6  43262  jm2.19  43421  rmydioph  43442  expdiophlem1  43449  expdioph  43451  lnr2i  43544  lpirlnr  43545  hbtlem2  43552  hbtlem4  43554  hbtlem6  43557  dgrsub2  43563  dgraa0p  43577  rngunsnply  43597  nlimsuc  43868  dfsucon  43950  radcnvrat  44741  pm14.24  44859  addrcom  44901  modelaxreplem1  45405  ormklocald  47304  natlocalincr  47306  afveu  47601  dfafn5b  47609  rlimdmafv  47625  afv2eu  47686  rlimdmafv2  47706  el1fzopredsuc  47774  minusmod5ne  47803  modmknepk  47816  elsetpreimafvssdm  47846  imasetpreimafvbijlemfo  47865  sprvalpw  47940  prprvalpw  47975  reupr  47982  fmtnofac2lem  48031  proththdlem  48076  perfectALTVlem2  48198  perfectALTV  48199  gbowpos  48235  gbowgt5  48238  gboge9  48240  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  uhgrimedgi  48366  isuspgrim0  48370  isuspgrimlem  48371  upgrimpths  48385  clnbgrgrim  48410  grimedg  48411  grtrissvtx  48420  stgredgiun  48434  stgrvtx0  48438  isubgr3stgrlem7  48448  grlimgrtrilem2  48478  gpgiedgdmellem  48522  gpgvtxel2  48524  gpgvtx0  48529  gpgvtx1  48530  gpgusgralem  48532  gpgedgvtx0  48537  gpgedgvtx1  48538  gpgedg2ov  48542  gpgedg2iv  48543  gpgnbgrvtx0  48550  gpgnbgrvtx1  48551  pgnbgreunbgr  48601  ringcinvALTV  48786  lincellss  48902  lindsrng01  48944  suppdm  48986  nnpw2pb  49063  0aryfvalel  49110  0aryfvalelfv  49111  itsclc0xyqsolr  49245  infsubc  49535  infsubc2  49536