Theorem syl5ibrcom 246

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  biimprcd  249  elsn2g  4666  preq1b  4847  elpreqprb  4868  reusv3  5403  alxfr  5405  reuhypd  5417  opth1  5475  euotd  5513  otiunsndisj  5520  tz7.2  5660  frsn  5763  dmopab2rex  5917  elsnxp  6290  reuop  6292  dfpo2  6295  ordtri1  6397  ordtri3  6400  fvmptdv2  7016  fveqressseq  7081  foco2  7110  fsn  7135  fnsnb  7166  fmptsng  7168  fmptsnd  7169  fconst2g  7206  fnprb  7212  fntpb  7213  funfvima  7234  soisoi  7328  isores3  7335  eqfunresadj  7360  riotaeqimp  7395  eusvobj2  7404  ovmpodv2  7569  f1opw2  7665  sorpssun  7724  sorpssin  7725  oneqmin  7792  nlimsucg  7835  onzsl  7839  tfinds  7853  funcnvuni  7926  opiota  8049  mposn  8093  frpoins3xpg  8130  frpoins3xp3g  8131  poxp2  8133  xpord2pred  8135  sexp2  8136  poxp3  8140  xpord3pred  8142  sexp3  8143  xpord3inddlem  8144  suppssov1  8187  suppssfv  8191  brtpos  8224  frrlem12  8286  frrlem13  8287  wfrlem10OLD  8322  wfrlem14OLD  8326  wfrlem15OLD  8327  seqomlem1  8454  seqomlem2  8455  omordi  8570  omord  8572  omwordi  8575  oeeui  8606  nnmordi  8635  nnmord  8636  nnmwordi  8639  nnawordex  8641  nnaordex  8642  nneob  8659  omsmolem  8660  eldifsucnn  8667  qsss  8776  eroveu  8810  mapsncnv  8891  ralxpmap  8894  elixpsn  8935  ixpsnf1o  8936  boxcutc  8939  pw2f1olem  9080  2pwne  9137  mapxpen  9147  mapunen  9150  php  9214  phpOLD  9226  onomeneq  9232  unxpdomlem2  9255  en1eqsnbi  9280  isfiniteg  9308  fofinf1o  9331  f1opwfi  9360  elfiun  9429  oieu  9538  brwdom2  9572  wdomtr  9574  ixpiunwdom  9589  en3lplem1  9611  suc11reg  9618  inf3lemd  9626  cantnfvalf  9664  cantnflt  9671  cantnfp1lem3  9679  cantnflem2  9689  ttrcltr  9715  rnttrcl  9721  ttrclselem1  9724  r1tr  9775  updjud  9933  dfac8alem  10028  wdomnumr  10063  isinfcard  10091  aceq3lem  10119  dfac5lem4  10125  dfac5  10127  dfac2b  10129  coftr  10272  fin23lem28  10339  fin23lem29  10340  fin1a2lem11  10409  fin1a2lem12  10410  fin1a2lem13  10411  hsmexlem9  10424  axdclem  10518  pwcfsdom  10582  gchdomtri  10628  fpwwe2  10642  gchpwdom  10669  gchhar  10678  addnidpi  10900  nqereu  10928  genpv  10998  genpdm  11001  distrlem5pr  11026  mulrid  11217  ltne  11316  mul02  11397  cnegex  11400  mul0or  11859  negfi  12168  sup2  12175  supaddc  12186  supadd  12187  supmul1  12188  supmul  12191  creur  12211  creui  12212  cju  12213  nnsub  12261  un0addcl  12510  un0mulcl  12511  nn0sub  12527  elz2  12581  zaddcl  12607  suprzcl2  12927  qmulz  12940  qre  12942  qnegcl  12955  elpqb  12965  xrmax1  13159  xrmin2  13162  max1ALT  13170  xlesubadd  13247  xmulass  13271  xlemul1a  13272  xrsupexmnf  13289  xrinfmexpnf  13290  xrub  13296  iccid  13374  fzsn  13548  fzsuc2  13564  fz1sbc  13582  elfzp12  13585  modmuladd  13883  seqid3  14017  bcval5  14283  bcpasc  14286  hashbnd  14301  hashnnn0genn0  14308  hashprg  14360  hashfzo  14394  wrdl1s1  14569  ccats1alpha  14574  cats1un  14676  shftlem  15020  replim  15068  absmod0  15255  absz  15263  rlimdm  15500  summolem2  15667  summo  15668  zsum  15669  fsum  15671  fsummulc2  15735  fsumconst  15741  fsum00  15749  incexclem  15787  isumsplit  15791  infcvgaux1i  15808  prodmolem2  15884  prodmo  15885  zprod  15886  fprod  15890  prodsn  15911  prodsnf  15913  fprodconst  15927  ruclem2  16180  fzo0dvdseq  16271  bitsf1ocnv  16390  sadcaddlem  16403  smueqlem  16436  gcdabs1  16475  bezoutlem1  16486  bezoutlem3  16488  bezoutlem4  16489  dvdsgcd  16491  dvdsmulgcd  16502  lcmgcdeq  16554  lcmf  16575  lcmfunsnlem1  16579  lcmfunsnlem2lem2  16581  isprm2lem  16623  dvdsprime  16629  isprm5  16649  coprm  16653  prmdvdsexpr  16659  rpexp  16664  phibndlem  16708  dfphi2  16712  hashgcdlem  16726  odzdvds  16733  nnoddn2prm  16749  pythagtriplem1  16754  iserodd  16773  pceulem  16783  pcqmul  16791  pcqcl  16794  pcxnn0cl  16798  pcxcl  16799  pcneg  16812  pcabs  16813  pcgcd1  16815  pcz  16819  pcprmpw2  16820  pcprmpw  16821  dvdsprmpweqle  16824  difsqpwdvds  16825  pcaddlem  16826  pcadd  16827  pcmpt  16830  pockthg  16844  prmreclem5  16858  4sqlem4  16890  mul4sq  16892  vdwapun  16912  vdwlem2  16920  vdwlem6  16924  vdwlem8  16926  vdwlem13  16931  0ram  16958  ram0  16960  ramcl  16967  cshwsiun  17038  wunress  17200  wunressOLD  17201  firest  17383  isssc  17772  pospo  18303  latnlej  18414  gsumval2a  18611  xpsmnd0  18701  mnd1id  18703  0subm  18735  mulgnn0p1  19002  mulgnn0ass  19027  cyccom  19119  gicsubgen  19194  symg1bas  19300  snsymgefmndeq  19304  psgnunilem1  19403  psgnunilem2  19405  mndodcongi  19453  oddvdsnn0  19454  odnncl  19455  oddvds  19457  odeq  19460  odeq1  19470  pgpfi2  19516  sylow2a  19529  sylow2blem3  19532  sylow3lem6  19542  lsmelvalm  19561  lsmsubm  19563  lsmsubg  19564  lsmmod  19585  lsmdisj2  19592  efgmnvl  19624  efgtlen  19636  efgs1b  19646  efgrelexlemb  19660  efgredeu  19662  efgcpbllemb  19665  frgpuptinv  19681  frgpup3lem  19687  qusabl  19775  frgpnabllem1  19783  cyggeninv  19793  cyggenod  19794  gsumval3eu  19814  dprdssv  19928  dprdfeq0  19934  dprdsubg  19936  dprddisj2  19951  ablfacrp  19978  pgpfac1lem3  19989  pgpfaclem2  19994  xpsring1d  20222  dvreq1  20303  irredn1  20318  nzrunit  20414  drngmul0or  20530  isabvd  20572  abvdom  20590  issrngd  20613  lmodfopnelem2  20654  lss1d  20719  lspsneq0  20768  lbspss  20838  lsmcl  20839  lvecvs0or  20867  lspindpi  20891  lidl1el  20991  lpiss  21089  lidldvgen  21094  rrgeq0  21107  domneq0  21114  qsssubdrg  21205  zringlpirlem1  21234  pzriprnglem6  21256  pzriprnglem12  21262  znfld  21336  znunit  21339  znrrg  21341  cygznlem3  21345  frgpcyg  21349  psgnghm  21353  ipeq0  21411  cssincl  21461  lsmcss  21465  obselocv  21503  dsmmacl  21516  dsmmlss  21519  mplsubrglem  21783  mplmonmul  21811  mplcoe5lem  21814  mhpsclcl  21910  mhpvarcl  21911  coe1tmmul2  22019  coe1tmmul  22020  pf1ind  22095  mat1dimelbas  22194  mdetralt  22331  mdetunilem2  22336  mdetunilem7  22341  mdetunilem9  22343  maducoeval2  22363  chpscmat  22565  chfacfscmulgsum  22583  chfacfpmmulgsum  22587  istopon  22635  eltg3  22686  tgidm  22704  clsval2  22775  opncldf1  22809  restbas  22883  tgrest  22884  restcld  22897  restcldr  22899  restcls  22906  restntr  22907  ordtbas2  22916  ordtbas  22917  ordtrest2lem  22928  ordtrest2  22929  pnfnei  22945  mnfnei  22946  tgcn  22977  cnconst  23009  cnindis  23017  lmss  23023  ordtt1  23104  discmp  23123  1stcrest  23178  2ndcdisj  23181  cldllycmp  23220  txbas  23292  ptpjpre1  23296  ptuni2  23301  ptbasin  23302  ptbasfi  23306  ptopn2  23309  txbasval  23331  ptpjopn  23337  ptclsg  23340  dfac14lem  23342  xkoccn  23344  ptcnp  23347  upxp  23348  ptrescn  23364  txkgen  23377  xkoptsub  23379  xkopt  23380  xkoco1cn  23382  xkoco2cn  23383  xkococn  23385  xkoinjcn  23412  ordthmeolem  23526  ptuncnv  23532  nrmhaus  23551  fbssint  23563  fbfinnfr  23566  fbasrn  23609  isufil2  23633  filufint  23645  rnelfm  23678  fmfnfmlem2  23680  fmfnfmlem3  23681  fmfnfmlem4  23682  fmfnfm  23683  flimtopon  23695  flimclslem  23709  fclstopon  23737  fclscf  23750  flimfnfcls  23753  alexsublem  23769  alexsubALTlem3  23774  alexsubALTlem4  23775  ptcmplem2  23778  tmdgsum2  23821  symgtgp  23831  cldsubg  23836  qustgplem  23846  tgptsmscld  23876  tsmsxplem1  23878  imasdsf1olem  24100  blssps  24151  blss  24152  stdbdxmet  24245  methaus  24250  metrest  24254  nrginvrcn  24430  nmoeq0  24474  blssioo  24532  xrtgioo  24543  xrsxmet  24546  reconnlem1  24563  reconnlem2  24564  xrge0tsms  24571  elcncf1di  24636  iccpnfcnv  24690  evth  24706  lebnumlem1  24708  lebnumlem2  24709  lebnumlem3  24710  nmoleub3  24867  minveclem3b  25177  ivthlem2  25202  ivthlem3  25203  elovolm  25225  ovolmge0  25227  ovoliun  25255  ovolicc2lem3  25269  ovolicc2  25272  voliunlem3  25302  dyaddisj  25346  dyadmax  25348  opnmblALT  25353  ismbfd  25389  ismbf2d  25390  mbfimaopnlem  25405  mbfimaopn2  25407  i1fmullem  25444  i1fres  25456  itg1climres  25465  mbfi1fseqlem4  25469  itg2lcl  25478  itgsplitioo  25588  ellimc2  25627  rolle  25743  dvlip  25746  dvge0  25759  dvne0  25764  lhop1lem  25766  tdeglem4  25813  tdeglem4OLD  25814  degltlem1  25826  deg1nn0clb  25844  deg1lt0  25845  dvdsq1p  25914  ply1rem  25917  fta1g  25921  elply2  25946  plyf  25948  ne0p  25957  plyeq0lem  25960  plypf1  25962  0dgrb  25996  coe1termlem  26008  dgrcolem2  26025  plymul0or  26031  plyrem  26055  fta1  26058  quotcan  26059  aalioulem3  26084  eff1olem  26294  lognegb  26335  eflogeq  26347  argregt0  26355  argrege0  26356  tanarg  26364  cxpexp  26413  cxpeq0  26423  mulcxp  26430  cxpeq  26502  atans2  26673  scvxcvx  26727  dmgmaddn0  26764  isppw2  26856  vmappw  26857  vmacl  26859  efvmacl  26861  isnsqf  26876  mumullem2  26921  sqff1o  26923  dvdsppwf1o  26927  ppiublem1  26942  vmalelog  26945  chtublem  26951  fsumvma  26953  perfectlem2  26970  perfect  26971  bposlem1  27024  lgsmod  27063  lgsne0  27075  lgsdirnn0  27084  lgsqr  27091  lgsdchr  27095  gausslemma2dlem1a  27105  gausslemma2dlem6  27112  lgseisenlem2  27116  lgsquadlem1  27120  lgsquadlem2  27121  2lgslem1b  27132  2sqlem2  27158  mul2sq  27159  2sqlem7  27164  dchrisum0fno1  27251  pntrsumbnd2  27307  ostthlem1  27367  ostth2lem2  27374  ostth3  27378  ostth  27379  nolesgn2ores  27412  nogesgn1ores  27414  nolt02o  27435  nogt01o  27436  nosupbnd2  27456  noinfbnd2lem1  27470  noetasuplem4  27476  noetainflem4  27480  maxs1  27505  mins2  27508  sltne  27510  ssltsn  27531  cuteq1  27572  madef  27589  sltlpss  27639  lrrecfr  27666  addsval  27685  addsproplem2  27693  addsuniflem  27724  negsid  27755  negsunif  27769  mulsproplem5  27816  mulsproplem6  27817  mulsproplem7  27818  mulsproplem8  27819  mulsproplem9  27820  slemuld  27834  ssltmul1  27842  ssltmul2  27843  sltmul2  27863  precsexlem8  27900  precsexlem9  27901  precsexlem11  27903  elons2  27925  colinearalg  28436  axpasch  28467  axlowdimlem16  28483  axlowdimlem17  28484  axlowdim  28487  axcontlem2  28491  axcontlem4  28493  axcontlem7  28496  lpvtx  28596  edglnl  28671  numedglnl  28672  usgredgop  28698  usgrexmplef  28784  uhgrspansubgrlem  28815  uhgrspan1  28828  nbusgredgeu0  28893  nb3grprlem2  28906  cusgrsize2inds  28978  vtxd0nedgb  29013  rusgrpropnb  29108  upgrwlkvtxedg  29170  wlkp1lem1  29198  wlkp1lem6  29203  wlkp1lem8  29205  usgr2wlkneq  29281  crctcshwlk  29344  crctcsh  29346  iswwlksnon  29375  wlkiswwlks1  29389  wwlksnextbi  29416  wwlksnextproplem2  29432  wspthsnonn0vne  29439  clwlkclwwlklem2  29521  clwwisshclwws  29536  erclwwlktr  29543  clwwlkel  29567  clwwlkext2edg  29577  erclwwlkntr  29592  clwlknf1oclwwlknlem2  29603  clwlknf1oclwwlknlem3  29604  clwlknf1oclwwlkn  29605  clwwlknonccat  29617  0wlkons1  29642  3wlkdlem6  29686  eupth2eucrct  29738  frgrwopreglem2  29834  2clwwlk2clwwlk  29871  wlkl0  29888  nvmul0or  30171  ipasslem5  30356  ipasslem11  30361  hvmul0or  30546  his6  30620  hhssnv  30785  ocsh  30804  ocin  30817  shsidmi  30905  chnlen0  30965  h1de2bi  31075  h1de2ctlem  31076  h1de2ci  31077  spansni  31078  3oalem1  31183  nmcexi  31547  atcveq0  31869  chcv1  31876  cdjreui  31953  cdj3lem2b  31958  xrge0tsmsd  32480  1fldgenq  32683  ccfldextdgrr  33036  ordtrest2NEWlem  33201  ordtrest2NEW  33202  xrge0iifcnv  33212  esumc  33348  esumpcvgval  33375  ballotlemfc0  33790  ballotlemfcc  33791  subfacp1lem4  34473  subfacp1lem5  34474  erdszelem8  34488  sconnpi1  34529  cvmsss2  34564  cvmlift2lem12  34604  satfv0  34648  satfv0fun  34661  satf00  34664  sat1el2xp  34669  fmla0xp  34673  fmlasucdisj  34689  satffunlem1lem1  34692  satffunlem2lem1  34694  dmopab3rexdif  34695  msubco  34821  msubvrs  34850  sinccvglem  34956  untsucf  34984  nnuni  35001  dfrdg2  35072  colineardim1  35338  btwnconn1lem14  35377  segleantisym  35392  colinbtwnle  35395  outsidele  35409  lineunray  35424  linethru  35430  elicc3  35506  opnregcld  35519  cldregopn  35520  fnejoin2  35558  bj-isrvec  36479  dissneqlem  36525  icorempo  36536  relowlssretop  36548  relowlpssretop  36549  rdgssun  36563  finxpsuclem  36582  lindsenlbs  36787  ptrecube  36792  poimirlem6  36798  poimirlem7  36799  poimirlem16  36808  poimirlem17  36809  poimirlem19  36811  poimirlem20  36812  poimirlem21  36813  poimirlem22  36814  poimirlem23  36815  poimirlem24  36816  poimirlem25  36817  poimirlem26  36818  poimirlem27  36819  poimirlem29  36821  poimirlem30  36822  poimirlem31  36823  poimirlem32  36824  itg2addnclem3  36845  ftc1anclem6  36870  dvasin  36876  unirep  36886  sdclem2  36914  ssbnd  36960  prdsbnd  36965  cntotbnd  36968  heibor1lem  36981  rrnequiv  37007  ismndo2  37046  grpoeqdivid  37053  isdrngo3  37131  crngohomfo  37178  0idl  37197  1idl  37198  divrngidl  37200  smprngopr  37224  prnc  37239  ispridlc  37242  riotaclbgBAD  38128  lshpdisj  38161  lsateln0  38169  lsatcveq0  38206  opnlen0  38362  cmtbr4N  38429  cvrnbtwn2  38449  cvrnbtwn4  38453  atcvreq0  38488  cvlatexch1  38510  exatleN  38579  atlelt  38613  ps-2  38653  llnn0  38691  lplnn0N  38722  islpln2a  38723  lvoln0N  38766  islvol2aN  38767  4at  38788  dalemcea  38835  dalem3  38839  pmapglb2N  38946  pmapglb2xN  38947  cdlema1N  38966  cdlemb  38969  paddasslem17  39011  llnexchb2lem  39043  llnexchb2  39044  lhpat3  39221  ltrnid  39310  trlne  39360  cdlemc4  39369  cdleme11h  39441  cdlemednuN  39475  cdlemg1a  39745  tendoeq2  39949  tendoid0  40000  dva1dim  40160  dib1dim  40340  dihlatat  40512  dochkrshp4  40564  dochkr1  40653  lclkrlem2e  40686  lcfrlem16  40733  lcfrlem28  40745  mapd0  40840  hdmap14lem13  41055  fnsnbt  41358  eqresfnbd  41361  f1o2d2  41362  frlmsnic  41413  evlselvlem  41461  dvdsexpnn0  41535  reladdrsub  41561  sn-negex12  41592  sn-mullid  41611  sn-mul02  41616  nn0addcom  41626  nn0mulcom  41630  zmulcomlem  41631  mulgt0con1d  41634  mulgt0con2d  41635  sn-sup2  41645  prjspner1  41671  elrfi  41735  mrefg2  41748  eldiophb  41798  eldioph2b  41804  diophin  41813  diophun  41814  rexzrexnn0  41845  eldioph4b  41852  diophren  41854  rencldnfilem  41861  pellexlem6  41875  jm2.19  42035  rmydioph  42056  expdiophlem1  42063  expdioph  42065  lnr2i  42161  lpirlnr  42162  hbtlem2  42169  hbtlem4  42171  hbtlem6  42174  dgrsub2  42180  dgraa0p  42194  rngunsnply  42218  nlimsuc  42495  dfsucon  42577  radcnvrat  43376  pm14.24  43494  addrcom  43537  natlocalincr  45889  afveu  46160  dfafn5b  46168  rlimdmafv  46184  afv2eu  46245  rlimdmafv2  46265  el1fzopredsuc  46332  elsetpreimafvssdm  46353  imasetpreimafvbijlemfo  46372  sprvalpw  46447  prprvalpw  46482  reupr  46489  fmtnofac2lem  46535  proththdlem  46580  perfectALTVlem2  46689  perfectALTV  46690  gbowpos  46726  gbowgt5  46729  gboge9  46731  nnsum4primesodd  46763  nnsum4primesoddALTV  46764  isomuspgr  46801  ringcinv  47019  ringcinvALTV  47043  lincellss  47195  lindsrng01  47237  suppdm  47279  nnpw2pb  47361  0aryfvalel  47408  0aryfvalelfv  47409  itsclc0xyqsolr  47543