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  elsn2g  4668  preq1b  4850  elpreqprb  4872  reusv3  5410  alxfr  5412  reuhypd  5424  axpr  5432  opth1  5485  euotd  5522  otiunsndisj  5529  tz7.2  5671  frsn  5775  dmopab2rex  5930  elsnxp  6312  reuop  6314  dfpo2  6317  ordtri1  6418  ordtri3  6421  fvmptdv2  7033  fveqressseq  7098  foco2  7128  fsn  7154  fnsnb  7185  fmptsng  7187  fmptsnd  7188  fconst2g  7222  fnprb  7227  fntpb  7228  funfvima  7249  soisoi  7347  isores3  7354  eqfunresadj  7379  riotaeqimp  7413  eusvobj2  7422  ovmpodv2  7590  f1opw2  7687  sorpssun  7748  sorpssin  7749  oneqmin  7819  nlimsucg  7862  onzsl  7866  tfinds  7880  funcnvuni  7954  mptcnfimad  8009  opiota  8082  mposn  8126  frpoins3xpg  8163  frpoins3xp3g  8164  poxp2  8166  xpord2pred  8168  sexp2  8169  poxp3  8173  xpord3pred  8175  sexp3  8176  xpord3inddlem  8177  suppssov1  8220  suppssov2  8221  suppssfv  8225  brtpos  8258  frrlem12  8320  frrlem13  8321  wfrlem10OLD  8356  wfrlem14OLD  8360  wfrlem15OLD  8361  seqomlem1  8488  seqomlem2  8489  omordi  8602  omord  8604  omwordi  8607  oeeui  8638  nnmordi  8667  nnmord  8668  nnmwordi  8671  nnawordex  8673  nnaordex  8674  nneob  8692  omsmolem  8693  eldifsucnn  8700  qsss  8816  eroveu  8850  mapsncnv  8931  ralxpmap  8934  elixpsn  8975  ixpsnf1o  8976  boxcutc  8979  pw2f1olem  9114  2pwne  9171  mapxpen  9181  mapunen  9184  php  9244  phpOLD  9256  onomeneq  9262  unxpdomlem2  9284  en1eqsnbi  9307  isfiniteg  9334  fofinf1o  9369  f1opwfi  9393  elfiun  9467  oieu  9576  brwdom2  9610  wdomtr  9612  ixpiunwdom  9627  en3lplem1  9649  suc11reg  9656  inf3lemd  9664  cantnfvalf  9702  cantnflt  9709  cantnfp1lem3  9717  cantnflem2  9727  ttrcltr  9753  rnttrcl  9759  ttrclselem1  9762  r1tr  9813  updjud  9971  dfac8alem  10066  wdomnumr  10101  isinfcard  10129  aceq3lem  10157  dfac5lem4  10163  dfac5lem4OLD  10165  dfac5  10166  dfac2b  10168  coftr  10310  fin23lem28  10377  fin23lem29  10378  fin1a2lem11  10447  fin1a2lem12  10448  fin1a2lem13  10449  hsmexlem9  10462  axdclem  10556  pwcfsdom  10620  gchdomtri  10666  fpwwe2  10680  gchpwdom  10707  gchhar  10716  addnidpi  10938  nqereu  10966  genpv  11036  genpdm  11039  distrlem5pr  11064  mulrid  11256  ltne  11355  mul02  11436  cnegex  11439  mul0or  11900  negfi  12214  sup2  12221  supaddc  12232  supadd  12233  supmul1  12234  supmul  12237  creur  12257  creui  12258  cju  12259  nnsub  12307  un0addcl  12556  un0mulcl  12557  nn0sub  12573  elz2  12628  zaddcl  12654  suprzcl2  12977  qmulz  12990  qre  12992  qnegcl  13005  elpqb  13015  xrmax1  13213  xrmin2  13216  max1ALT  13224  xlesubadd  13301  xmulass  13325  xlemul1a  13326  xrsupexmnf  13343  xrinfmexpnf  13344  xrub  13350  iccid  13428  fzsn  13602  fzsuc2  13618  fz1sbc  13636  elfzp12  13639  modmuladd  13950  seqid3  14083  bcval5  14353  bcpasc  14356  hashbnd  14371  hashnnn0genn0  14378  hashprg  14430  hashfzo  14464  tpfo  14535  wrdl1s1  14648  ccats1alpha  14653  cats1un  14755  s7f1o  15001  shftlem  15103  replim  15151  absmod0  15338  absz  15346  rlimdm  15583  summolem2  15748  summo  15749  zsum  15750  fsum  15752  fsummulc2  15816  fsumconst  15822  fsum00  15830  incexclem  15868  isumsplit  15872  infcvgaux1i  15889  prodmolem2  15967  prodmo  15968  zprod  15969  fprod  15973  prodsn  15994  prodsnf  15996  fprodconst  16010  ruclem2  16264  fzo0dvdseq  16356  bitsf1ocnv  16477  sadcaddlem  16490  smueqlem  16523  gcdabs1  16562  bezoutlem1  16572  bezoutlem3  16574  bezoutlem4  16575  dvdsgcd  16577  dvdsmulgcd  16589  lcmgcdeq  16645  lcmf  16666  lcmfunsnlem1  16670  lcmfunsnlem2lem2  16672  isprm2lem  16714  dvdsprime  16720  isprm5  16740  coprm  16744  prmdvdsexpr  16750  rpexp  16755  phibndlem  16803  dfphi2  16807  hashgcdlem  16821  odzdvds  16828  nnoddn2prm  16844  pythagtriplem1  16849  iserodd  16868  pceulem  16878  pcqmul  16886  pcqcl  16889  pcxnn0cl  16893  pcxcl  16894  pcneg  16907  pcabs  16908  pcgcd1  16910  pcz  16914  pcprmpw2  16915  pcprmpw  16916  dvdsprmpweqle  16919  difsqpwdvds  16920  pcaddlem  16921  pcadd  16922  pcmpt  16925  pockthg  16939  prmreclem5  16953  4sqlem4  16985  mul4sq  16987  vdwapun  17007  vdwlem2  17015  vdwlem6  17019  vdwlem8  17021  vdwlem13  17026  0ram  17053  ram0  17055  ramcl  17062  cshwsiun  17133  wunress  17295  wunressOLD  17296  firest  17478  isssc  17867  pospo  18402  latnlej  18513  gsumval2a  18710  xpsmnd0  18803  mnd1id  18805  0subm  18842  mulgnn0p1  19115  mulgnn0ass  19140  cyccom  19233  gicsubgen  19309  symg1bas  19422  snsymgefmndeq  19426  psgnunilem1  19525  psgnunilem2  19527  mndodcongi  19575  oddvdsnn0  19576  odnncl  19577  oddvds  19579  odeq  19582  odeq1  19592  pgpfi2  19638  sylow2a  19651  sylow2blem3  19654  sylow3lem6  19664  lsmelvalm  19683  lsmsubm  19685  lsmsubg  19686  lsmmod  19707  lsmdisj2  19714  efgmnvl  19746  efgtlen  19758  efgs1b  19768  efgrelexlemb  19782  efgredeu  19784  efgcpbllemb  19787  frgpuptinv  19803  frgpup3lem  19809  qusabl  19897  frgpnabllem1  19905  cyggeninv  19915  cyggenod  19916  gsumval3eu  19936  dprdssv  20050  dprdfeq0  20056  dprdsubg  20058  dprddisj2  20073  ablfacrp  20100  pgpfac1lem3  20111  pgpfaclem2  20116  xpsring1d  20346  dvreq1  20427  irredn1  20442  nzrunit  20540  ringcinv  20687  rrgeq0  20716  domneq0  20724  drngmul0orOLD  20777  isabvd  20829  abvdom  20847  issrngd  20872  lmodfopnelem2  20913  lss1d  20978  lspsneq0  21027  lbspss  21098  lsmcl  21099  lvecvs0or  21127  lspindpi  21151  lidl1el  21253  lpiss  21356  lidldvgen  21361  qsssubdrg  21461  zringlpirlem1  21490  pzriprnglem6  21514  pzriprnglem12  21520  znfld  21596  znunit  21599  znrrg  21601  cygznlem3  21605  frgpcyg  21609  psgnghm  21615  ipeq0  21673  cssincl  21723  lsmcss  21727  obselocv  21765  dsmmacl  21778  dsmmlss  21781  mplsubrglem  22041  mplmonmul  22071  mplcoe5lem  22074  mhpsclcl  22168  mhpvarcl  22169  psdmul  22187  coe1tmmul2  22294  coe1tmmul  22295  pf1ind  22374  mat1dimelbas  22492  mdetralt  22629  mdetunilem2  22634  mdetunilem7  22639  mdetunilem9  22641  maducoeval2  22661  chpscmat  22863  chfacfscmulgsum  22881  chfacfpmmulgsum  22885  istopon  22933  eltg3  22984  tgidm  23002  clsval2  23073  opncldf1  23107  restbas  23181  tgrest  23182  restcld  23195  restcldr  23197  restcls  23204  restntr  23205  ordtbas2  23214  ordtbas  23215  ordtrest2lem  23226  ordtrest2  23227  pnfnei  23243  mnfnei  23244  tgcn  23275  cnconst  23307  cnindis  23315  lmss  23321  ordtt1  23402  discmp  23421  1stcrest  23476  2ndcdisj  23479  cldllycmp  23518  txbas  23590  ptpjpre1  23594  ptuni2  23599  ptbasin  23600  ptbasfi  23604  ptopn2  23607  txbasval  23629  ptpjopn  23635  ptclsg  23638  dfac14lem  23640  xkoccn  23642  ptcnp  23645  upxp  23646  ptrescn  23662  txkgen  23675  xkoptsub  23677  xkopt  23678  xkoco1cn  23680  xkoco2cn  23681  xkococn  23683  xkoinjcn  23710  ordthmeolem  23824  ptuncnv  23830  nrmhaus  23849  fbssint  23861  fbfinnfr  23864  fbasrn  23907  isufil2  23931  filufint  23943  rnelfm  23976  fmfnfmlem2  23978  fmfnfmlem3  23979  fmfnfmlem4  23980  fmfnfm  23981  flimtopon  23993  flimclslem  24007  fclstopon  24035  fclscf  24048  flimfnfcls  24051  alexsublem  24067  alexsubALTlem3  24072  alexsubALTlem4  24073  ptcmplem2  24076  tmdgsum2  24119  symgtgp  24129  cldsubg  24134  qustgplem  24144  tgptsmscld  24174  tsmsxplem1  24176  imasdsf1olem  24398  blssps  24449  blss  24450  stdbdxmet  24543  methaus  24548  metrest  24552  nrginvrcn  24728  nmoeq0  24772  blssioo  24830  xrtgioo  24841  xrsxmet  24844  reconnlem1  24861  reconnlem2  24862  xrge0tsms  24869  elcncf1di  24934  iccpnfcnv  24988  evth  25004  lebnumlem1  25006  lebnumlem2  25007  lebnumlem3  25008  nmoleub3  25165  minveclem3b  25475  ivthlem2  25500  ivthlem3  25501  elovolm  25523  ovolmge0  25525  ovoliun  25553  ovolicc2lem3  25567  ovolicc2  25570  voliunlem3  25600  dyaddisj  25644  dyadmax  25646  opnmblALT  25651  ismbfd  25687  ismbf2d  25688  mbfimaopnlem  25703  mbfimaopn2  25705  i1fmullem  25742  i1fres  25754  itg1climres  25763  mbfi1fseqlem4  25767  itg2lcl  25776  itgsplitioo  25887  ellimc2  25926  rolle  26042  dvlip  26046  dvge0  26059  dvne0  26064  lhop1lem  26066  tdeglem4  26113  degltlem1  26125  deg1nn0clb  26143  deg1lt0  26144  dvdsq1p  26216  ply1rem  26219  fta1g  26223  elply2  26249  plyf  26251  ne0p  26260  plyeq0lem  26263  plypf1  26265  0dgrb  26299  coe1termlem  26311  dgrcolem2  26328  plymul0or  26336  plyrem  26361  fta1  26364  quotcan  26365  aalioulem3  26390  eff1olem  26604  lognegb  26646  eflogeq  26658  argregt0  26666  argrege0  26667  tanarg  26675  cxpexp  26724  cxpeq0  26734  mulcxp  26741  cxpeq  26814  atans2  26988  scvxcvx  27043  dmgmaddn0  27080  isppw2  27172  vmappw  27173  vmacl  27175  efvmacl  27177  isnsqf  27192  mumullem2  27237  sqff1o  27239  dvdsppwf1o  27243  ppiublem1  27260  vmalelog  27263  chtublem  27269  fsumvma  27271  perfectlem2  27288  perfect  27289  bposlem1  27342  lgsmod  27381  lgsne0  27393  lgsdirnn0  27402  lgsqr  27409  lgsdchr  27413  gausslemma2dlem1a  27423  gausslemma2dlem6  27430  lgseisenlem2  27434  lgsquadlem1  27438  lgsquadlem2  27439  2lgslem1b  27450  2sqlem2  27476  mul2sq  27477  2sqlem7  27482  dchrisum0fno1  27569  pntrsumbnd2  27625  ostthlem1  27685  ostth2lem2  27692  ostth3  27696  ostth  27697  nolesgn2ores  27731  nogesgn1ores  27733  nolt02o  27754  nogt01o  27755  nosupbnd2  27775  noinfbnd2lem1  27789  noetasuplem4  27795  noetainflem4  27799  maxs1  27824  mins2  27827  sltne  27829  ssltsn  27851  cuteq1  27892  madef  27909  sltlpss  27959  lrrecfr  27990  addsval  28009  addsproplem2  28017  addsuniflem  28048  addsbdaylem  28063  negsid  28087  negsunif  28101  mulsproplem5  28160  mulsproplem6  28161  mulsproplem7  28162  mulsproplem8  28163  mulsproplem9  28164  slemuld  28178  ssltmul1  28187  ssltmul2  28188  sltmul2  28211  muls0ord  28225  precsexlem8  28252  precsexlem9  28253  precsexlem11  28255  elons2  28295  onaddscl  28300  onmulscl  28301  nnsge1  28360  n0subs  28374  dfnns2  28376  znegscl  28392  zaddscl  28394  zmulscld  28397  elzn0s  28398  eln0zs  28400  n0seo  28419  zseo  28420  zs12bday  28438  recut  28442  0reno  28443  remulscllem1  28446  colinearalg  28939  axpasch  28970  axlowdimlem16  28986  axlowdimlem17  28987  axlowdim  28990  axcontlem2  28994  axcontlem4  28996  axcontlem7  28999  lpvtx  29099  edglnl  29174  numedglnl  29175  usgredgop  29201  usgrexmplef  29290  uhgrspansubgrlem  29321  uhgrspan1  29334  nbusgredgeu0  29399  nb3grprlem2  29412  cusgrsize2inds  29485  vtxd0nedgb  29520  rusgrpropnb  29615  upgrwlkvtxedg  29677  wlkp1lem1  29705  wlkp1lem6  29710  wlkp1lem8  29712  usgr2wlkneq  29788  crctcshwlk  29851  crctcsh  29853  iswwlksnon  29882  wlkiswwlks1  29896  wwlksnextbi  29923  wwlksnextproplem2  29939  wspthsnonn0vne  29946  clwlkclwwlklem2  30028  clwwisshclwws  30043  erclwwlktr  30050  clwwlkel  30074  clwwlkext2edg  30084  erclwwlkntr  30099  clwlknf1oclwwlknlem2  30110  clwlknf1oclwwlknlem3  30111  clwlknf1oclwwlkn  30112  clwwlknonccat  30124  0wlkons1  30149  3wlkdlem6  30193  eupth2eucrct  30245  frgrwopreglem2  30341  2clwwlk2clwwlk  30378  wlkl0  30395  nvmul0or  30678  ipasslem5  30863  ipasslem11  30868  hvmul0or  31053  his6  31127  hhssnv  31292  ocsh  31311  ocin  31324  shsidmi  31412  chnlen0  31472  h1de2bi  31582  h1de2ctlem  31583  h1de2ci  31584  spansni  31585  3oalem1  31690  nmcexi  32054  atcveq0  32376  chcv1  32383  cdjreui  32460  cdj3lem2b  32465  xrge0tsmsd  33047  1fldgenq  33303  ccfldextdgrr  33696  ordtrest2NEWlem  33882  ordtrest2NEW  33883  xrge0iifcnv  33893  esumc  34031  esumpcvgval  34058  ballotlemfc0  34473  ballotlemfcc  34474  gblacfnacd  35091  subfacp1lem4  35167  subfacp1lem5  35168  erdszelem8  35182  sconnpi1  35223  cvmsss2  35258  cvmlift2lem12  35298  satfv0  35342  satfv0fun  35355  satf00  35358  sat1el2xp  35363  fmla0xp  35367  fmlasucdisj  35383  satffunlem1lem1  35386  satffunlem2lem1  35388  dmopab3rexdif  35389  msubco  35515  msubvrs  35544  ellcsrspsn  35625  sinccvglem  35656  untsucf  35689  nnuni  35706  dfrdg2  35776  colineardim1  36042  btwnconn1lem14  36081  segleantisym  36096  colinbtwnle  36099  outsidele  36113  lineunray  36128  linethru  36134  elicc3  36299  opnregcld  36312  cldregopn  36313  fnejoin2  36351  bj-isrvec  37276  dissneqlem  37322  icorempo  37333  relowlssretop  37345  relowlpssretop  37346  rdgssun  37360  finxpsuclem  37379  lindsenlbs  37601  ptrecube  37606  poimirlem6  37612  poimirlem7  37613  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem21  37627  poimirlem22  37628  poimirlem23  37629  poimirlem24  37630  poimirlem25  37631  poimirlem26  37632  poimirlem27  37633  poimirlem29  37635  poimirlem30  37636  poimirlem31  37637  poimirlem32  37638  itg2addnclem3  37659  ftc1anclem6  37684  dvasin  37690  unirep  37700  sdclem2  37728  ssbnd  37774  prdsbnd  37779  cntotbnd  37782  heibor1lem  37795  rrnequiv  37821  ismndo2  37860  grpoeqdivid  37867  isdrngo3  37945  crngohomfo  37992  0idl  38011  1idl  38012  divrngidl  38014  smprngopr  38038  prnc  38053  ispridlc  38056  riotaclbgBAD  38935  lshpdisj  38968  lsateln0  38976  lsatcveq0  39013  opnlen0  39169  cmtbr4N  39236  cvrnbtwn2  39256  cvrnbtwn4  39260  atcvreq0  39295  cvlatexch1  39317  exatleN  39386  atlelt  39420  ps-2  39460  llnn0  39498  lplnn0N  39529  islpln2a  39530  lvoln0N  39573  islvol2aN  39574  4at  39595  dalemcea  39642  dalem3  39646  pmapglb2N  39753  pmapglb2xN  39754  cdlema1N  39773  cdlemb  39776  paddasslem17  39818  llnexchb2lem  39850  llnexchb2  39851  lhpat3  40028  ltrnid  40117  trlne  40167  cdlemc4  40176  cdleme11h  40248  cdlemednuN  40282  cdlemg1a  40552  tendoeq2  40756  tendoid0  40807  dva1dim  40967  dib1dim  41147  dihlatat  41319  dochkrshp4  41371  dochkr1  41460  lclkrlem2e  41493  lcfrlem16  41540  lcfrlem28  41552  mapd0  41647  hdmap14lem13  41862  fnsnbt  42249  eqresfnbd  42251  f1o2d2  42252  expeq1d  42337  expeqidd  42338  dvdsexpnn0  42347  reladdrsub  42391  sn-negex12  42422  sn-mullid  42441  sn-mul02  42446  nn0addcom  42456  nn0mulcom  42460  zmulcomlem  42461  mulgt0con1d  42464  mulgt0con2d  42465  sn-sup2  42477  frlmsnic  42526  evlselvlem  42572  prjspner1  42612  elrfi  42681  mrefg2  42694  eldiophb  42744  eldioph2b  42750  diophin  42759  diophun  42760  rexzrexnn0  42791  eldioph4b  42798  diophren  42800  rencldnfilem  42807  pellexlem6  42821  jm2.19  42981  rmydioph  43002  expdiophlem1  43009  expdioph  43011  lnr2i  43104  lpirlnr  43105  hbtlem2  43112  hbtlem4  43114  hbtlem6  43117  dgrsub2  43123  dgraa0p  43137  rngunsnply  43157  nlimsuc  43430  dfsucon  43512  radcnvrat  44309  pm14.24  44427  addrcom  44470  modelaxreplem1  44942  natlocalincr  46829  afveu  47102  dfafn5b  47110  rlimdmafv  47126  afv2eu  47187  rlimdmafv2  47207  el1fzopredsuc  47274  minusmod5ne  47288  elsetpreimafvssdm  47310  imasetpreimafvbijlemfo  47329  sprvalpw  47404  prprvalpw  47439  reupr  47446  fmtnofac2lem  47492  proththdlem  47537  perfectALTVlem2  47646  perfectALTV  47647  gbowpos  47683  gbowgt5  47686  gboge9  47688  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  isuspgrim0  47809  isuspgrimlem  47811  clnbgrgrim  47839  grimedg  47840  grtrissvtx  47848  stgredgiun  47860  stgrvtx0  47864  isubgr3stgrlem7  47874  grlimgrtrilem2  47897  gpgvtxel2  47941  gpgedgel  47942  gpgvtx0  47943  gpgvtx1  47944  gpgusgralem  47945  gpgedgvtx0  47953  gpgedgvtx1  47954  gpg3nbgrvtxlem  47957  gpgnbgrvtx0  47964  gpgnbgrvtx1  47965  ringcinvALTV  48153  lincellss  48271  lindsrng01  48313  suppdm  48355  nnpw2pb  48436  0aryfvalel  48483  0aryfvalelfv  48484  itsclc0xyqsolr  48618