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  4503  elsn2g  4630  preq1b  4812  elpreqprb  4834  reusv3  5362  alxfr  5364  reuhypd  5376  axpr  5384  opth1  5437  euotd  5475  otiunsndisj  5482  tz7.2  5623  frsn  5728  dmopab2rex  5883  elsnxp  6266  reuop  6268  dfpo2  6271  ordtri1  6367  ordtri3  6370  fvmptdv2  6988  fveqressseq  7053  foco2  7083  fsn  7109  fnsnbg  7140  fnsnbOLD  7142  fmptsng  7144  fmptsnd  7145  fconst2g  7179  fnprb  7184  fntpb  7185  funfvima  7206  soisoi  7305  isores3  7312  eqfunresadj  7337  riotaeqimp  7372  eusvobj2  7381  ovmpodv2  7549  f1opw2  7646  sorpssun  7708  sorpssin  7709  oneqmin  7778  nlimsucg  7820  onzsl  7824  tfinds  7838  funcnvuni  7910  mptcnfimad  7967  opiota  8040  mposn  8084  frpoins3xpg  8121  frpoins3xp3g  8122  poxp2  8124  xpord2pred  8126  sexp2  8127  poxp3  8131  xpord3pred  8133  sexp3  8134  xpord3inddlem  8135  suppssov1  8178  suppssov2  8179  suppssfv  8183  brtpos  8216  frrlem12  8278  frrlem13  8279  seqomlem1  8420  seqomlem2  8421  omordi  8532  omord  8534  omwordi  8537  oeeui  8568  nnmordi  8597  nnmord  8598  nnmwordi  8601  nnawordex  8603  nnaordex  8604  nneob  8622  omsmolem  8623  eldifsucnn  8630  qsss  8751  eroveu  8787  mapsncnv  8868  ralxpmap  8871  elixpsn  8912  ixpsnf1o  8913  boxcutc  8916  pw2f1olem  9049  2pwne  9102  mapxpen  9112  mapunen  9115  php  9176  onomeneq  9183  unxpdomlem2  9204  en1eqsnbi  9227  isfiniteg  9254  fofinf1o  9289  f1opwfi  9313  elfiun  9387  oieu  9498  brwdom2  9532  wdomtr  9534  ixpiunwdom  9549  en3lplem1  9571  suc11reg  9578  inf3lemd  9586  cantnfvalf  9624  cantnflt  9631  cantnfp1lem3  9639  cantnflem2  9649  ttrcltr  9675  rnttrcl  9681  ttrclselem1  9684  r1tr  9735  updjud  9893  dfac8alem  9988  wdomnumr  10023  isinfcard  10051  aceq3lem  10079  dfac5lem4  10085  dfac5lem4OLD  10087  dfac5  10088  dfac2b  10090  coftr  10232  fin23lem28  10299  fin23lem29  10300  fin1a2lem11  10369  fin1a2lem12  10370  fin1a2lem13  10371  hsmexlem9  10384  axdclem  10478  pwcfsdom  10542  gchdomtri  10588  fpwwe2  10602  gchpwdom  10629  gchhar  10638  addnidpi  10860  nqereu  10888  genpv  10958  genpdm  10961  distrlem5pr  10986  mulrid  11178  ltne  11277  mul02  11358  cnegex  11361  mul0or  11824  negfi  12138  sup2  12145  supaddc  12156  supadd  12157  supmul1  12158  supmul  12161  creur  12181  creui  12182  cju  12183  nnsub  12231  un0addcl  12481  un0mulcl  12482  nn0sub  12498  elz2  12553  zaddcl  12579  suprzcl2  12903  qmulz  12916  qre  12918  qnegcl  12931  elpqb  12941  xrmax1  13141  xrmin2  13144  max1ALT  13152  xlesubadd  13229  xmulass  13253  xlemul1a  13254  xrsupexmnf  13271  xrinfmexpnf  13272  xrub  13278  iccid  13357  fzsn  13533  fzsuc2  13549  fz1sbc  13567  elfzp12  13570  modmuladd  13884  seqid3  14017  bcval5  14289  bcpasc  14292  hashbnd  14307  hashnnn0genn0  14314  hashprg  14366  hashfzo  14400  tpfo  14471  wrdl1s1  14585  ccats1alpha  14590  cats1un  14692  s7f1o  14938  shftlem  15040  replim  15088  absmod0  15275  absz  15283  rlimdm  15523  summolem2  15688  summo  15689  zsum  15690  fsum  15692  fsummulc2  15756  fsumconst  15762  fsum00  15770  incexclem  15808  isumsplit  15812  infcvgaux1i  15829  prodmolem2  15907  prodmo  15908  zprod  15909  fprod  15913  prodsn  15934  prodsnf  15936  fprodconst  15950  ruclem2  16206  fzo0dvdseq  16299  bitsf1ocnv  16420  sadcaddlem  16433  smueqlem  16466  gcdabs1  16505  bezoutlem1  16515  bezoutlem3  16517  bezoutlem4  16518  dvdsgcd  16520  dvdsmulgcd  16532  lcmgcdeq  16588  lcmf  16609  lcmfunsnlem1  16613  lcmfunsnlem2lem2  16615  isprm2lem  16657  dvdsprime  16663  isprm5  16683  coprm  16687  prmdvdsexpr  16693  rpexp  16698  phibndlem  16746  dfphi2  16750  hashgcdlem  16764  odzdvds  16772  nnoddn2prm  16788  pythagtriplem1  16793  iserodd  16812  pceulem  16822  pcqmul  16830  pcqcl  16833  pcxnn0cl  16837  pcxcl  16838  pcneg  16851  pcabs  16852  pcgcd1  16854  pcz  16858  pcprmpw2  16859  pcprmpw  16860  dvdsprmpweqle  16863  difsqpwdvds  16864  pcaddlem  16865  pcadd  16866  pcmpt  16869  pockthg  16883  prmreclem5  16897  4sqlem4  16929  mul4sq  16931  vdwapun  16951  vdwlem2  16959  vdwlem6  16963  vdwlem8  16965  vdwlem13  16970  0ram  16997  ram0  16999  ramcl  17006  cshwsiun  17076  wunress  17225  firest  17401  isssc  17788  pospo  18310  latnlej  18421  gsumval2a  18618  xpsmnd0  18711  mnd1id  18713  0subm  18750  mulgnn0p1  19023  mulgnn0ass  19048  cyccom  19141  gicsubgen  19217  symg1bas  19327  snsymgefmndeq  19331  psgnunilem1  19429  psgnunilem2  19431  mndodcongi  19479  oddvdsnn0  19480  odnncl  19481  oddvds  19483  odeq  19486  odeq1  19496  pgpfi2  19542  sylow2a  19555  sylow2blem3  19558  sylow3lem6  19568  lsmelvalm  19587  lsmsubm  19589  lsmsubg  19590  lsmmod  19611  lsmdisj2  19618  efgmnvl  19650  efgtlen  19662  efgs1b  19672  efgrelexlemb  19686  efgredeu  19688  efgcpbllemb  19691  frgpuptinv  19707  frgpup3lem  19713  qusabl  19801  frgpnabllem1  19809  cyggeninv  19819  cyggenod  19820  gsumval3eu  19840  dprdssv  19954  dprdfeq0  19960  dprdsubg  19962  dprddisj2  19977  ablfacrp  20004  pgpfac1lem3  20015  pgpfaclem2  20020  xpsring1d  20248  dvreq1  20326  irredn1  20341  nzrunit  20439  ringcinv  20586  rrgeq0  20615  domneq0  20623  drngmul0orOLD  20676  isabvd  20727  abvdom  20745  issrngd  20770  lmodfopnelem2  20811  lss1d  20875  lspsneq0  20924  lbspss  20995  lsmcl  20996  lvecvs0or  21024  lspindpi  21048  lidl1el  21142  lpiss  21245  lidldvgen  21250  qsssubdrg  21349  zringlpirlem1  21378  pzriprnglem6  21402  pzriprnglem12  21408  znfld  21476  znunit  21479  znrrg  21481  cygznlem3  21485  frgpcyg  21489  psgnghm  21495  ipeq0  21553  cssincl  21603  lsmcss  21607  obselocv  21643  dsmmacl  21656  dsmmlss  21659  mplsubrglem  21919  mplmonmul  21949  mplcoe5lem  21952  mhpsclcl  22040  mhpvarcl  22041  psdmul  22059  coe1tmmul2  22168  coe1tmmul  22169  pf1ind  22248  mat1dimelbas  22364  mdetralt  22501  mdetunilem2  22506  mdetunilem7  22511  mdetunilem9  22513  maducoeval2  22533  chpscmat  22735  chfacfscmulgsum  22753  chfacfpmmulgsum  22757  istopon  22805  eltg3  22855  tgidm  22873  clsval2  22943  opncldf1  22977  restbas  23051  tgrest  23052  restcld  23065  restcldr  23067  restcls  23074  restntr  23075  ordtbas2  23084  ordtbas  23085  ordtrest2lem  23096  ordtrest2  23097  pnfnei  23113  mnfnei  23114  tgcn  23145  cnconst  23177  cnindis  23185  lmss  23191  ordtt1  23272  discmp  23291  1stcrest  23346  2ndcdisj  23349  cldllycmp  23388  txbas  23460  ptpjpre1  23464  ptuni2  23469  ptbasin  23470  ptbasfi  23474  ptopn2  23477  txbasval  23499  ptpjopn  23505  ptclsg  23508  dfac14lem  23510  xkoccn  23512  ptcnp  23515  upxp  23516  ptrescn  23532  txkgen  23545  xkoptsub  23547  xkopt  23548  xkoco1cn  23550  xkoco2cn  23551  xkococn  23553  xkoinjcn  23580  ordthmeolem  23694  ptuncnv  23700  nrmhaus  23719  fbssint  23731  fbfinnfr  23734  fbasrn  23777  isufil2  23801  filufint  23813  rnelfm  23846  fmfnfmlem2  23848  fmfnfmlem3  23849  fmfnfmlem4  23850  fmfnfm  23851  flimtopon  23863  flimclslem  23877  fclstopon  23905  fclscf  23918  flimfnfcls  23921  alexsublem  23937  alexsubALTlem3  23942  alexsubALTlem4  23943  ptcmplem2  23946  tmdgsum2  23989  symgtgp  23999  cldsubg  24004  qustgplem  24014  tgptsmscld  24044  tsmsxplem1  24046  imasdsf1olem  24267  blssps  24318  blss  24319  stdbdxmet  24409  methaus  24414  metrest  24418  nrginvrcn  24586  nmoeq0  24630  blssioo  24689  xrtgioo  24701  xrsxmet  24704  reconnlem1  24721  reconnlem2  24722  xrge0tsms  24729  elcncf1di  24794  iccpnfcnv  24848  evth  24864  lebnumlem1  24866  lebnumlem2  24867  lebnumlem3  24868  nmoleub3  25025  minveclem3b  25334  ivthlem2  25359  ivthlem3  25360  elovolm  25382  ovolmge0  25384  ovoliun  25412  ovolicc2lem3  25426  ovolicc2  25429  voliunlem3  25459  dyaddisj  25503  dyadmax  25505  opnmblALT  25510  ismbfd  25546  ismbf2d  25547  mbfimaopnlem  25562  mbfimaopn2  25564  i1fmullem  25601  i1fres  25612  itg1climres  25621  mbfi1fseqlem4  25625  itg2lcl  25634  itgsplitioo  25745  ellimc2  25784  rolle  25900  dvlip  25904  dvge0  25917  dvne0  25922  lhop1lem  25924  tdeglem4  25971  degltlem1  25983  deg1nn0clb  26001  deg1lt0  26002  dvdsq1p  26074  ply1rem  26077  fta1g  26081  elply2  26107  plyf  26109  ne0p  26118  plyeq0lem  26121  plypf1  26123  0dgrb  26157  coe1termlem  26169  dgrcolem2  26186  plymul0or  26194  plyrem  26219  fta1  26222  quotcan  26223  aalioulem3  26248  eff1olem  26463  lognegb  26505  eflogeq  26517  argregt0  26525  argrege0  26526  tanarg  26534  cxpexp  26583  cxpeq0  26593  mulcxp  26600  cxpeq  26673  atans2  26847  scvxcvx  26902  dmgmaddn0  26939  isppw2  27031  vmappw  27032  vmacl  27034  efvmacl  27036  isnsqf  27051  mumullem2  27096  sqff1o  27098  dvdsppwf1o  27102  ppiublem1  27119  vmalelog  27122  chtublem  27128  fsumvma  27130  perfectlem2  27147  perfect  27148  bposlem1  27201  lgsmod  27240  lgsne0  27252  lgsdirnn0  27261  lgsqr  27268  lgsdchr  27272  gausslemma2dlem1a  27282  gausslemma2dlem6  27289  lgseisenlem2  27293  lgsquadlem1  27297  lgsquadlem2  27298  2lgslem1b  27309  2sqlem2  27335  mul2sq  27336  2sqlem7  27341  dchrisum0fno1  27428  pntrsumbnd2  27484  ostthlem1  27544  ostth2lem2  27551  ostth3  27555  ostth  27556  nolesgn2ores  27590  nogesgn1ores  27592  nolt02o  27613  nogt01o  27614  nosupbnd2  27634  noinfbnd2lem1  27648  noetasuplem4  27654  noetainflem4  27658  maxs1  27683  mins2  27686  sltne  27688  ssltsn  27710  cuteq1  27752  madef  27770  sltlpss  27825  lrrecfr  27856  addsval  27875  addsproplem2  27883  addsuniflem  27914  addsbdaylem  27929  negsid  27953  negsunif  27967  mulsproplem5  28029  mulsproplem6  28030  mulsproplem7  28031  mulsproplem8  28032  mulsproplem9  28033  slemuld  28047  ssltmul1  28056  ssltmul2  28057  sltmul2  28080  muls0ord  28094  precsexlem8  28122  precsexlem9  28123  precsexlem11  28125  elons2  28165  onscutlt  28171  bdayon  28179  onaddscl  28180  onmulscl  28181  nnsge1  28241  n0sfincut  28252  n0subs  28259  dfnns2  28267  eucliddivs  28271  znegscl  28286  zaddscl  28288  zmulscld  28291  elzn0s  28292  eln0zs  28294  n0seo  28313  zseo  28314  zs12negscl  28346  zs12ge0  28348  zs12bday  28349  recut  28353  0reno  28354  remulscllem1  28357  colinearalg  28843  axpasch  28874  axlowdimlem16  28890  axlowdimlem17  28891  axlowdim  28894  axcontlem2  28898  axcontlem4  28900  axcontlem7  28903  lpvtx  29001  edglnl  29076  numedglnl  29077  usgredgop  29103  usgrexmplef  29192  uhgrspansubgrlem  29223  uhgrspan1  29236  nbusgredgeu0  29301  nb3grprlem2  29314  cusgrsize2inds  29387  vtxd0nedgb  29422  rusgrpropnb  29517  upgrwlkvtxedg  29579  wlkp1lem1  29607  wlkp1lem6  29612  wlkp1lem8  29614  usgr2wlkneq  29692  crctcshwlk  29758  crctcsh  29760  iswwlksnon  29789  wlkiswwlks1  29803  wwlksnextbi  29830  wwlksnextproplem2  29846  wspthsnonn0vne  29853  clwlkclwwlklem2  29935  clwwisshclwws  29950  erclwwlktr  29957  clwwlkel  29981  clwwlkext2edg  29991  erclwwlkntr  30006  clwlknf1oclwwlknlem2  30017  clwlknf1oclwwlknlem3  30018  clwlknf1oclwwlkn  30019  clwwlknonccat  30031  0wlkons1  30056  3wlkdlem6  30100  eupth2eucrct  30152  frgrwopreglem2  30248  2clwwlk2clwwlk  30285  wlkl0  30302  nvmul0or  30585  ipasslem5  30770  ipasslem11  30775  hvmul0or  30960  his6  31034  hhssnv  31199  ocsh  31218  ocin  31231  shsidmi  31319  chnlen0  31379  h1de2bi  31489  h1de2ctlem  31490  h1de2ci  31491  spansni  31492  3oalem1  31597  nmcexi  31961  atcveq0  32283  chcv1  32290  cdjreui  32367  cdj3lem2b  32372  xrge0tsmsd  33008  1fldgenq  33278  ccfldextdgrr  33673  ordtrest2NEWlem  33918  ordtrest2NEW  33919  xrge0iifcnv  33929  esumc  34047  esumpcvgval  34074  ballotlemfc0  34490  ballotlemfcc  34491  gblacfnacd  35095  subfacp1lem4  35170  subfacp1lem5  35171  erdszelem8  35185  sconnpi1  35226  cvmsss2  35261  cvmlift2lem12  35301  satfv0  35345  satfv0fun  35358  satf00  35361  sat1el2xp  35366  fmla0xp  35370  fmlasucdisj  35386  satffunlem1lem1  35389  satffunlem2lem1  35391  dmopab3rexdif  35392  msubco  35518  msubvrs  35547  ellcsrspsn  35628  sinccvglem  35659  untsucf  35692  nnuni  35709  dfrdg2  35778  colineardim1  36044  btwnconn1lem14  36083  segleantisym  36098  colinbtwnle  36101  outsidele  36115  lineunray  36130  linethru  36136  elicc3  36300  opnregcld  36313  cldregopn  36314  fnejoin2  36352  bj-isrvec  37277  dissneqlem  37323  icorempo  37334  relowlssretop  37346  relowlpssretop  37347  rdgssun  37361  finxpsuclem  37380  lindsenlbs  37604  ptrecube  37609  poimirlem6  37615  poimirlem7  37616  poimirlem16  37625  poimirlem17  37626  poimirlem19  37628  poimirlem20  37629  poimirlem21  37630  poimirlem22  37631  poimirlem23  37632  poimirlem24  37633  poimirlem25  37634  poimirlem26  37635  poimirlem27  37636  poimirlem29  37638  poimirlem30  37639  poimirlem31  37640  poimirlem32  37641  itg2addnclem3  37662  ftc1anclem6  37687  dvasin  37693  unirep  37703  sdclem2  37731  ssbnd  37777  prdsbnd  37782  cntotbnd  37785  heibor1lem  37798  rrnequiv  37824  ismndo2  37863  grpoeqdivid  37870  isdrngo3  37948  crngohomfo  37995  0idl  38014  1idl  38015  divrngidl  38017  smprngopr  38041  prnc  38056  ispridlc  38059  riotaclbgBAD  38942  lshpdisj  38975  lsateln0  38983  lsatcveq0  39020  opnlen0  39176  cmtbr4N  39243  cvrnbtwn2  39263  cvrnbtwn4  39267  atcvreq0  39302  cvlatexch1  39324  exatleN  39393  atlelt  39427  ps-2  39467  llnn0  39505  lplnn0N  39536  islpln2a  39537  lvoln0N  39580  islvol2aN  39581  4at  39602  dalemcea  39649  dalem3  39653  pmapglb2N  39760  pmapglb2xN  39761  cdlema1N  39780  cdlemb  39783  paddasslem17  39825  llnexchb2lem  39857  llnexchb2  39858  lhpat3  40035  ltrnid  40124  trlne  40174  cdlemc4  40183  cdleme11h  40255  cdlemednuN  40289  cdlemg1a  40559  tendoeq2  40763  tendoid0  40814  dva1dim  40974  dib1dim  41154  dihlatat  41326  dochkrshp4  41378  dochkr1  41467  lclkrlem2e  41500  lcfrlem16  41547  lcfrlem28  41559  mapd0  41654  hdmap14lem13  41869  eqresfnbd  42215  f1o2d2  42216  expeq1d  42307  expeqidd  42308  dvdsexpnn0  42317  reladdrsub  42368  sn-remul0ord  42391  sn-negex12  42400  sn-mullid  42419  sn-mul02  42435  nn0addcom  42445  nn0mulcom  42449  zmulcomlem  42450  mulgt0con1d  42453  mulgt0con2d  42454  sn-sup2  42472  frlmsnic  42521  evlselvlem  42567  prjspner1  42607  elrfi  42675  mrefg2  42688  eldiophb  42738  eldioph2b  42744  diophin  42753  diophun  42754  rexzrexnn0  42785  eldioph4b  42792  diophren  42794  rencldnfilem  42801  pellexlem6  42815  jm2.19  42975  rmydioph  42996  expdiophlem1  43003  expdioph  43005  lnr2i  43098  lpirlnr  43099  hbtlem2  43106  hbtlem4  43108  hbtlem6  43111  dgrsub2  43117  dgraa0p  43131  rngunsnply  43151  nlimsuc  43423  dfsucon  43505  radcnvrat  44296  pm14.24  44414  addrcom  44457  modelaxreplem1  44961  ormklocald  46865  natlocalincr  46867  afveu  47144  dfafn5b  47152  rlimdmafv  47168  afv2eu  47229  rlimdmafv2  47249  el1fzopredsuc  47316  minusmod5ne  47340  modmknepk  47353  elsetpreimafvssdm  47377  imasetpreimafvbijlemfo  47396  sprvalpw  47471  prprvalpw  47506  reupr  47513  fmtnofac2lem  47559  proththdlem  47604  perfectALTVlem2  47713  perfectALTV  47714  gbowpos  47750  gbowgt5  47753  gboge9  47755  nnsum4primesodd  47787  nnsum4primesoddALTV  47788  uhgrimedgi  47880  isuspgrim0  47884  isuspgrimlem  47885  upgrimpths  47899  clnbgrgrim  47924  grimedg  47925  grtrissvtx  47933  stgredgiun  47947  stgrvtx0  47951  isubgr3stgrlem7  47961  grlimgrtrilem2  47984  gpgiedgdmellem  48027  gpgvtxel2  48029  gpgvtx0  48034  gpgvtx1  48035  gpgusgralem  48037  gpgedgvtx0  48042  gpgedgvtx1  48043  gpgedg2ov  48047  gpgedg2iv  48048  gpgnbgrvtx0  48055  gpgnbgrvtx1  48056  pgnbgreunbgr  48105  ringcinvALTV  48288  lincellss  48405  lindsrng01  48447  suppdm  48489  nnpw2pb  48566  0aryfvalel  48613  0aryfvalelfv  48614  itsclc0xyqsolr  48748  infsubc  49037  infsubc2  49038