Theorem syl5ibrcom 250

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  biimprcd  253  iftrueb  4495  elsn2g  4625  preq1b  4806  elpreqprb  4828  reusv3  5370  alxfr  5372  reuhypd  5384  axpr  5392  opth1  5451  euotd  5490  otiunsndisj  5497  tz7.2  5638  frsn  5743  dmopab2rex  5901  elsnxp  6289  reuop  6291  dfpo2  6294  ordtri1  6391  ordtri3  6394  fvmptdv2  7005  fveqressseq  7072  foco2  7102  fsn  7129  fnsnbg  7162  fnsnbOLD  7164  fmptsng  7166  fmptsnd  7167  fconst2g  7202  fnprb  7207  fntpb  7208  funfvima  7229  soisoi  7329  isores3  7336  eqfunresadj  7363  riotaeqimp  7396  eusvobj2  7405  ovmpodv2  7571  f1opw2  7669  sorpssun  7731  sorpssin  7732  oneqmin  7799  nlimsucg  7838  onzsl  7842  tfinds  7856  funcnvuni  7929  mptcnfimad  7983  opiota  8056  mposn  8100  mpof1o2d  8123  frpoins3xpg  8138  frpoins3xp3g  8139  poxp2  8141  xpord2pred  8143  sexp2  8144  poxp3  8148  xpord3pred  8150  sexp3  8151  xpord3inddlem  8152  suppssov1  8195  suppssov2  8196  suppssfv  8200  brtpos  8233  frrlem12  8296  frrlem13  8297  seqomlem1  8439  seqomlem2  8440  omordi  8553  omord  8555  omwordi  8558  oeeui  8590  nnmordi  8619  nnmord  8620  nnmwordi  8623  nnawordex  8625  nnaordex  8626  nneob  8644  omsmolem  8645  eldifsucnn  8652  qsss  8775  eroveu  8812  mapsncnv  8900  ralxpmap  8903  elixpsn  8944  ixpsnf1o  8945  boxcutc  8948  pw2f1olem  9079  2pwne  9131  mapxpen  9141  mapunen  9144  php  9201  onomeneq  9208  unxpdomlem2  9227  en1eqsnbi  9246  isfiniteg  9270  fofinf1o  9299  f1opwfi  9323  elfiun  9400  oieu  9511  brwdom2  9545  wdomtr  9547  ixpiunwdom  9562  en3lplem1  9591  suc11reg  9598  inf3lemd  9606  cantnfvalf  9644  cantnflt  9651  cantnfp1lem3  9659  cantnflem2  9669  ttrcltr  9695  rnttrcl  9701  ttrclselem1  9704  r1tr  9758  updjud  9939  dfac8alem  10032  wdomnumr  10067  isinfcard  10095  aceq3lem  10123  dfac5lem4  10129  dfac5  10131  dfac2b  10133  coftr  10275  fin23lem28  10342  fin23lem29  10343  fin1a2lem11  10412  fin1a2lem12  10413  fin1a2lem13  10414  hsmexlem9  10427  axdclem  10521  pwcfsdom  10592  gchdomtri  10638  fpwwe2  10652  gchpwdom  10679  gchhar  10688  addnidpi  10910  nqereu  10938  genpv  11008  genpdm  11011  distrlem5pr  11036  mulrid  11230  ltne  11331  mul02  11412  cnegex  11415  mul0or  11878  negfi  12188  sup2  12195  supaddc  12206  supadd  12207  supmul1  12208  supmul  12211  creur  12236  creui  12237  cju  12238  nnsub  12304  un0addcl  12561  un0mulcl  12562  nn0sub  12578  elz2  12633  zaddcl  12658  suprzcl2  12987  qmulz  13000  qre  13002  qnegcl  13016  elpqb  13026  xrmax1  13227  xrmin2  13230  max1ALT  13238  xlesubadd  13315  xmulass  13339  xlemul1a  13340  xrsupexmnf  13357  xrinfmexpnf  13358  xrub  13364  iccid  13443  fzsn  13621  fzsuc2  13637  fz1sbc  13655  elfzp12  13658  modmuladd  13977  seqid3  14110  bcval5  14382  bcpasc  14385  hashbnd  14400  hashnnn0genn0  14407  hashprg  14459  hashfzo  14494  tpfo  14565  wrdl1s1  14682  ccats1alpha  14687  cats1un  14790  s7f1o  15039  shftlem  15141  replim  15203  absmod0  15390  absz  15398  rlimdm  15638  summolem2  15802  summo  15803  zsum  15804  fsum  15806  fsummulc2  15870  fsumconst  15876  fsum00  15885  incexclem  15925  isumsplit  15929  infcvgaux1i  15946  prodmolem2  16022  prodmo  16023  zprod  16024  fprod  16028  prodsn  16049  prodsnf  16051  fprodconst  16065  ruclem2  16320  fzo0dvdseq  16413  bitsf1ocnv  16534  sadcaddlem  16547  smueqlem  16580  gcdabs1  16619  bezoutlem1  16629  bezoutlem3  16631  bezoutlem4  16632  dvdsgcd  16634  dvdsmulgcd  16646  lcmgcdeq  16702  lcmf  16723  lcmfunsnlem1  16727  lcmfunsnlem2lem2  16729  isprm2lem  16771  dvdsprime  16777  isprm5  16798  coprm  16802  prmdvdsexpr  16808  rpexp  16813  phibndlem  16861  dfphi2  16865  hashgcdlem  16879  odzdvds  16887  nnoddn2prm  16903  pythagtriplem1  16908  iserodd  16927  pceulem  16937  pcqmul  16945  pcqcl  16948  pcxnn0cl  16952  pcxcl  16953  pcneg  16966  pcabs  16967  pcgcd1  16969  pcz  16973  pcprmpw2  16974  pcprmpw  16975  dvdsprmpweqle  16978  difsqpwdvds  16979  pcaddlem  16980  pcadd  16981  pcmpt  16984  pockthg  16998  prmreclem5  17012  4sqlem4  17044  mul4sq  17046  vdwapun  17066  vdwlem2  17074  vdwlem6  17078  vdwlem8  17080  vdwlem13  17085  0ram  17112  ram0  17114  ramcl  17121  cshwsiun  17191  wunress  17341  firest  17517  isssc  17909  pospo  18431  latnlej  18544  gsumval2a  18787  xpsmnd0  18885  mnd1id  18887  0subm  18926  mulgnn0p1  19208  mulgnn0ass  19233  cyccom  19331  gicsubgen  19406  symg1bas  19518  snsymgefmndeq  19522  psgnunilem1  19620  psgnunilem2  19622  mndodcongi  19670  oddvdsnn0  19671  odnncl  19672  oddvds  19674  odeq  19677  odeq1  19687  pgpfi2  19733  sylow2a  19746  sylow2blem3  19749  sylow3lem6  19759  lsmelvalm  19778  lsmsubm  19780  lsmsubg  19781  lsmmod  19802  lsmdisj2  19809  efgmnvl  19841  efgtlen  19853  efgs1b  19863  efgrelexlemb  19877  efgredeu  19879  efgcpbllemb  19882  frgpuptinv  19898  frgpup3lem  19904  qusabl  19992  frgpnabllem1  20000  cyggeninv  20010  cyggenod  20011  gsumval3eu  20031  dprdssv  20145  dprdfeq0  20151  dprdsubg  20153  dprddisj2  20168  ablfacrp  20195  pgpfac1lem3  20206  pgpfaclem2  20211  xpsring1d  20474  dvreq1  20552  irredn1  20567  crngrhmfo  20637  nzrunit  20685  ringcinv  20833  rrgeq0  20862  domneq0  20870  isdrng5  20917  isabvd  20978  abvdom  20996  issrngd  21021  lmodfopnelem2  21083  lss1d  21147  lspsneq0  21196  lbspss  21266  lsmcl  21267  lvecvs0or  21295  lspindpi  21319  lidl1el  21414  rspsn0  21435  lpiss  21560  lidldvgen  21565  qsssubdrg  21639  zringlpirlem1  21675  pzriprnglem6  21699  pzriprnglem12  21705  znfld  21773  znunit  21776  znrrg  21778  cygznlem3  21782  frgpcyg  21786  psgnghm  21793  ipeq0  21851  cssincl  21901  lsmcss  21905  obselocv  21941  dsmmacl  21954  dsmmlss  21957  lindsenlbs  22064  mplsubrglem  22218  mplmonmul  22252  mplcoe5lem  22255  mhpsclcl  22375  mhpvarcl  22376  psdmul  22394  coe1tmmul2  22502  coe1tmmul  22503  pf1ind  22580  mat1dimelbas  22693  mdetralt  22830  mdetunilem2  22835  mdetunilem7  22840  mdetunilem9  22842  maducoeval2  22862  chpscmat  23067  chfacfscmulgsum  23085  chfacfpmmulgsum  23089  istopon  23137  eltg3  23187  tgidm  23205  clsval2  23275  opncldf1  23309  restbas  23383  tgrest  23384  restcld  23397  restcldr  23399  restcls  23406  restntr  23407  ordtbas2  23416  ordtbas  23417  ordtrest2lem  23428  ordtrest2  23429  pnfnei  23445  mnfnei  23446  tgcn  23477  cnconst  23509  cnindis  23517  lmss  23523  ordtt1  23604  discmp  23623  1stcrest  23678  2ndcdisj  23682  cldllycmp  23721  txbas  23793  ptpjpre1  23797  ptuni2  23802  ptbasin  23803  ptbasfi  23807  ptopn2  23810  txbasval  23832  ptpjopn  23838  ptclsg  23841  dfac14lem  23843  xkoccn  23845  ptcnp  23848  upxp  23849  ptrescn  23865  txkgen  23878  xkoptsub  23880  xkopt  23881  xkoco1cn  23883  xkoco2cn  23884  xkococn  23886  xkoinjcn  23913  ordthmeolem  24027  ptuncnv  24033  nrmhaus  24052  fbssint  24064  fbfinnfr  24067  fbasrn  24110  isufil2  24134  filufint  24146  rnelfm  24179  fmfnfmlem2  24181  fmfnfmlem3  24182  fmfnfmlem4  24183  fmfnfm  24184  flimtopon  24196  flimclslem  24210  fclstopon  24238  fclscf  24251  flimfnfcls  24254  alexsublem  24270  alexsubALTlem3  24275  alexsubALTlem4  24276  ptcmplem2  24279  tmdgsum2  24322  symgtgp  24332  cldsubg  24337  qustgplem  24347  tgptsmscld  24377  tsmsxplem1  24379  imasdsf1olem  24599  blssps  24650  blss  24651  stdbdxmet  24741  methaus  24746  metrest  24750  nrginvrcn  24918  nmoeq0  24962  blssioo  25021  xrtgioo  25033  xrsxmet  25036  reconnlem1  25053  reconnlem2  25054  xrge0tsms  25061  elcncf1di  25123  iccpnfcnv  25172  evth  25187  lebnumlem1  25189  lebnumlem2  25190  lebnumlem3  25191  nmoleub3  25347  minveclem3b  25656  ivthlem2  25680  ivthlem3  25681  elovolm  25703  ovolmge0  25705  ovoliun  25733  ovolicc2lem3  25747  ovolicc2  25750  voliunlem3  25780  dyaddisj  25824  dyadmax  25826  opnmblALT  25831  ismbfd  25867  ismbf2d  25868  mbfimaopnlem  25883  mbfimaopn2  25885  i1fmullem  25922  i1fres  25933  itg1climres  25942  mbfi1fseqlem4  25946  itg2lcl  25955  itgsplitioo  26065  ellimc2  26104  rolle  26217  dvlip  26220  dvge0  26233  dvne0  26238  lhop1lem  26240  tdeglem4  26285  degltlem1  26297  deg1nn0clb  26315  deg1lt0  26316  dvdsq1p  26388  ply1rem  26391  fta1g  26395  elply2  26421  plyf  26423  ne0p  26432  plyeq0lem  26436  plypf1  26438  0dgrb  26472  coe1termlem  26484  dgrcolem2  26500  plymul0or  26508  plyrem  26535  fta1  26538  rnplynfin  26539  quotcan  26541  aalioulem3  26570  eff1olem  26785  lognegb  26827  eflogeq  26839  argregt0  26847  argrege0  26848  tanarg  26856  cxpexp  26905  cxpeq0  26915  mulcxp  26922  cxpeq  26994  atans2  27168  scvxcvx  27222  dmgmaddn0  27259  isppw2  27351  vmappw  27352  vmacl  27354  efvmacl  27356  isnsqf  27371  mumullem2  27416  sqff1o  27418  dvdsppwf1o  27422  ppiublem1  27438  vmalelog  27441  chtublem  27447  fsumvma  27449  perfectlem2  27466  perfect  27467  bposlem1  27520  lgsmod  27559  lgsne0  27571  lgsdirnn0  27580  lgsqr  27587  lgsdchr  27591  gausslemma2dlem1a  27601  gausslemma2dlem6  27608  lgseisenlem2  27612  lgsquadlem1  27616  lgsquadlem2  27617  2lgslem1b  27628  2sqlem2  27654  mul2sq  27655  2sqlem7  27660  dchrisum0fno1  27747  pntrsumbnd2  27803  ostthlem1  27863  ostth2lem2  27870  ostth3  27874  ostth  27875  nolesgn2ores  27908  nogesgn1ores  27910  nolt02o  27931  nogt01o  27932  nosupbnd2  27952  noinfbnd2lem1  27966  noetasuplem4  27972  noetainflem4  27976  maxs1  28005  mins2  28008  ltsne  28010  eqcuts3  28069  cuteq1  28082  madef  28101  ltslpss  28173  lrrecfr  28208  addsval  28227  addsproplem2  28235  addsuniflem  28266  addbdaylem  28282  negsid  28306  negsunif  28320  mulsproplem5  28385  mulsproplem6  28386  mulsproplem7  28387  mulsproplem8  28388  mulsproplem9  28389  lemulsd  28403  sltmuls1  28412  sltmuls2  28413  ltmuls2  28436  muls0ord  28450  precsexlem8  28479  precsexlem9  28480  precsexlem11  28482  elons2  28523  oncutlt  28529  bdayons  28541  onaddscl  28542  onmulscl  28543  nnsge1  28608  n0fincut  28620  n0subs  28628  dfnns2  28637  eucliddivs  28641  znegscl  28657  zaddscl  28659  zmulscld  28662  elzn0s  28663  eln0zs  28665  n0seo  28686  zseo  28687  bdaypw2n0bndlem  28728  bdaypw2n0bnd  28729  z12no  28741  z12addscl  28742  z12negscl  28743  z12shalf  28745  z12zsodd  28747  z12sge0  28748  z12bdaylem  28749  bdayfinlem  28751  recut  28759  elreno2  28760  remulscllem1  28765  colinearalg  29367  axpasch  29398  axlowdimlem16  29414  axlowdimlem17  29415  axlowdim  29418  axcontlem2  29422  axcontlem4  29424  axcontlem7  29427  lpvtx  29525  edglnl  29600  numedglnl  29601  usgredgop  29630  usgrexmplef  29719  uhgrspansubgrlem  29750  uhgrspan1  29763  nbusgredgeu0  29828  nb3grprlem2  29841  cusgrsize2inds  29913  vtxd0nedgb  29948  rusgrpropnb  30043  upgrwlkvtxedg  30104  wlkp1lem1  30131  wlkp1lem6  30136  wlkp1lem8  30138  usgr2wlkneq  30221  crctcshwlk  30290  crctcsh  30292  iswwlksnon  30321  wlkiswwlks1  30335  wwlksnextbi  30362  wwlksnextproplem2  30378  wspthsnonn0vne  30385  clwlkclwwlklem2  30470  clwwisshclwws  30485  erclwwlktr  30492  clwwlkel  30516  clwwlkext2edg  30526  erclwwlkntr  30541  clwlknf1oclwwlknlem2  30552  clwlknf1oclwwlknlem3  30553  clwlknf1oclwwlkn  30554  clwwlknonccat  30566  0wlkons1  30591  3wlkdlem6  30645  eupth2eucrct  30697  frgrwopreglem2  30793  2clwwlk2clwwlk  30830  wlkl0  30847  nvmul0or  31131  ipasslem5  31316  ipasslem11  31321  hvmul0or  31506  his6  31580  hhssnv  31745  ocsh  31764  ocin  31777  shsidmi  31865  chnlen0  31925  h1de2bi  32035  h1de2ctlem  32036  h1de2ci  32037  spansni  32038  3oalem1  32143  nmcexi  32507  atcveq0  32829  chcv1  32836  cdjreui  32913  cdj3lem2b  32918  xrge0tsmsd  33513  1fldgenq  33763  psrmonmul  34060  ccfldextdgrr  34182  ordtrest2NEWlem  34432  ordtrest2NEW  34433  xrge0iifcnv  34443  esumc  34561  esumpcvgval  34588  ballotlemfc0  35004  ballotlemfcc  35005  fissorduni  35594  axprALT2  35617  fineqvnttrclse  35650  gblacfnacd  35699  vonf1oonfo  35712  onvfowev  35713  subfacp1lem4  35762  subfacp1lem5  35763  erdszelem8  35777  sconnpi1  35818  cvmsss2  35853  cvmlift2lem12  35893  satfv0  35937  satfv0fun  35950  satf00  35953  sat1el2xp  35958  fmla0xp  35962  fmlasucdisj  35978  satffunlem1lem1  35981  satffunlem2lem1  35983  dmopab3rexdif  35984  msubco  36110  msubvrs  36139  ellcsrspsn  36220  sinccvglem  36251  untsucf  36289  nnuni  36306  dfrdg2  36372  colineardim1  36641  btwnconn1lem14  36680  segleantisym  36695  colinbtwnle  36698  outsidele  36712  lineunray  36727  linethru  36733  nmulprop  36770  nmuladdss  36793  elicc3  36936  opnregcld  36949  cldregopn  36950  fnejoin2  36988  bj-isrvec  38046  dissneqlem  38094  icorempo  38105  relowlssretop  38117  relowlpssretop  38118  rdgssun  38132  finxpsuclem  38151  ptrecube  38369  poimirlem6  38375  poimirlem7  38376  poimirlem16  38385  poimirlem17  38386  poimirlem19  38388  poimirlem20  38389  poimirlem21  38390  poimirlem22  38391  poimirlem23  38392  poimirlem24  38393  poimirlem25  38394  poimirlem26  38395  poimirlem27  38396  poimirlem29  38398  poimirlem30  38399  poimirlem31  38400  poimirlem32  38401  itg2addnclem3  38422  ftc1anclem6  38447  dvasin  38453  unirep  38464  sdclem2  38492  ssbnd  38538  prdsbnd  38543  cntotbnd  38546  heibor1lem  38559  rrnequiv  38585  ismndo2  38624  grpoeqdivid  38631  isdrngo3  38709  crngohomfo  38756  0idl  38775  1idl  38776  divrngidl  38778  smprngopr  38802  prnc  38817  ispridlc  38820  disjimeceqim  39552  riotaclbgBAD  39827  lshpdisj  39860  lsateln0  39868  lsatcveq0  39905  opnlen0  40061  cmtbr4N  40128  cvrnbtwn2  40148  cvrnbtwn4  40152  atcvreq0  40187  cvlatexch1  40209  exatleN  40277  atlelt  40311  ps-2  40351  llnn0  40389  lplnn0N  40420  islpln2a  40421  lvoln0N  40464  islvol2aN  40465  4at  40486  dalemcea  40533  dalem3  40537  pmapglb2N  40644  pmapglb2xN  40645  cdlema1N  40664  cdlemb  40667  paddasslem17  40709  llnexchb2lem  40741  llnexchb2  40742  lhpat3  40919  ltrnid  41008  trlne  41058  cdlemc4  41067  cdleme11h  41139  cdlemednuN  41173  cdlemg1a  41443  tendoeq2  41647  tendoid0  41698  dva1dim  41858  dib1dim  42038  dihlatat  42210  dochkrshp4  42262  dochkr1  42351  lclkrlem2e  42384  lcfrlem16  42431  lcfrlem28  42443  mapd0  42538  hdmap14lem13  42753  eqresfnbd  43102  expeq1d  43199  expeqidd  43200  dvdsexpnn0  43209  reladdrsub  43260  sn-remul0ord  43283  sn-negex12  43292  sn-mullid  43311  sn-mul02  43340  nn0addcom  43350  nn0mulcom  43354  zmulcomlem  43355  mulgt0con1d  43358  mulgt0con2d  43359  sn-sup2  43379  frlmsnic  43422  evlselvlem  43434  prjspner1  43472  elrfi  43539  mrefg2  43552  eldiophb  43602  eldioph2b  43608  diophin  43617  diophun  43618  rexzrexnn0  43645  eldioph4b  43652  diophren  43654  rencldnfilem  43661  pellexlem6  43675  jm2.19  43834  rmydioph  43855  expdiophlem1  43862  expdioph  43864  lnr2i  43957  lpirlnr  43958  hbtlem2  43965  hbtlem4  43967  hbtlem6  43970  dgrsub2  43976  dgraa0p  43990  rngunsnply  44010  nlimsuc  44281  dfsucon  44363  radcnvrat  45138  pm14.24  45256  addrcom  45297  modelaxreplem1  45801  ormklocald  47704  afveu  48041  dfafn5b  48049  rlimdmafv  48065  afv2eu  48126  rlimdmafv2  48146  el1fzopredsuc  48214  minusmod5ne  48243  modmknepk  48256  elsetpreimafvssdm  48286  imasetpreimafvbijlemfo  48305  sprvalpw  48380  prprvalpw  48415  reupr  48422  fmtnofac2lem  48471  proththdlem  48516  perfectALTVlem2  48638  perfectALTV  48639  gbowpos  48675  gbowgt5  48678  gboge9  48680  nnsum4primesodd  48712  nnsum4primesoddALTV  48713  uhgrimedgi  48806  isuspgrim0  48810  isuspgrimlem  48811  upgrimpths  48825  clnbgrgrim  48850  grimedg  48851  grtrissvtx  48860  stgredgiun  48874  stgrvtx0  48878  isubgr3stgrlem7  48888  grlimgrtrilem2  48918  gpgiedgdmellem  48962  gpgvtxel2  48964  gpgvtx0  48969  gpgvtx1  48970  gpgusgralem  48972  gpgedgvtx0  48977  gpgedgvtx1  48978  gpgedg2ov  48982  gpgedg2iv  48983  gpgnbgrvtx0  48990  gpgnbgrvtx1  48991  pgnbgreunbgr  49041  ringcinvALTV  49225  smprngprmrng  49254  lincellss  49356  lindsrng01  49398  suppdm  49440  nnpw2pb  49517  0aryfvalel  49564  0aryfvalelfv  49565  itsclc0xyqsolr  49699  infsubc  49986  infsubc2  49987