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  5367  alxfr  5369  reuhypd  5381  axpr  5389  opth1  5444  euotd  5486  otiunsndisj  5493  tz7.2  5634  frsn  5739  dmopab2rex  5899  elsnxp  6293  reuop  6295  dfpo2  6298  ordtri1  6395  ordtri3  6398  fvmptdv2  7010  fveqressseq  7077  foco2  7107  fsn  7134  fnsnbg  7167  fnsnbOLD  7169  fmptsng  7171  fmptsnd  7172  fconst2g  7207  fnprb  7212  fntpb  7213  funfvima  7234  soisoi  7334  isores3  7341  eqfunresadj  7368  riotaeqimp  7401  eusvobj2  7410  ovmpodv2  7576  f1opw2  7674  sorpssun  7744  sorpssin  7745  oneqmin  7812  nlimsucg  7851  onzsl  7855  tfinds  7869  funcnvuni  7942  mptcnfimad  7996  opiota  8068  mposn  8112  mpof1o2d  8135  frpoins3xpg  8150  frpoins3xp3g  8151  poxp2  8153  xpord2pred  8155  sexp2  8156  poxp3  8160  xpord3pred  8162  sexp3  8163  xpord3inddlem  8164  suppssov1  8207  suppssov2  8208  suppssfv  8212  brtpos  8245  frrlem12  8308  frrlem13  8309  seqomlem1  8453  seqomlem2  8454  omordi  8567  omord  8569  omwordi  8572  oeeui  8604  nnmordi  8633  nnmord  8634  nnmwordi  8637  nnawordex  8639  nnaordex  8640  nneob  8658  omsmolem  8659  eldifsucnn  8666  qsss  8789  eroveu  8826  mapsncnv  8914  ralxpmap  8917  elixpsn  8958  ixpsnf1o  8959  boxcutc  8962  pw2f1olem  9093  2pwne  9145  mapxpen  9155  mapunen  9158  php  9215  onomeneq  9222  unxpdomlem2  9241  en1eqsnbi  9260  fissorduni  9275  isfiniteg  9285  fofinf1o  9314  f1opwfi  9338  elfiun  9415  oieu  9526  brwdom2  9560  wdomtr  9562  ixpiunwdom  9577  en3lplem1  9606  suc11reg  9613  inf3lemd  9621  cantnfvalf  9659  cantnflt  9666  cantnfp1lem3  9674  cantnflem2  9684  ttrcltr  9710  rnttrcl  9716  ttrclselem1  9719  r1tr  9776  updjud  10008  dfac8alem  10101  wdomnumr  10136  isinfcard  10164  aceq3lem  10192  dfac5lem4  10198  dfac5  10200  dfac2b  10202  coftr  10344  fin23lem28  10411  fin23lem29  10412  fin1a2lem11  10481  fin1a2lem12  10482  fin1a2lem13  10483  hsmexlem9  10496  axdclem  10590  pwcfsdom  10661  gchdomtri  10707  fpwwe2  10721  gchpwdom  10748  gchhar  10757  addnidpi  10979  nqereu  11007  genpv  11077  genpdm  11080  distrlem5pr  11105  mulrid  11299  ltne  11400  mul02  11481  cnegex  11484  mul0or  11949  negfi  12259  sup2  12266  supaddc  12277  supadd  12278  supmul1  12279  supmul  12282  creur  12307  creui  12308  cju  12309  nnsub  12375  un0addcl  12632  un0mulcl  12633  nn0sub  12649  elz2  12704  zaddcl  12729  suprzcl2  13058  qmulz  13071  qre  13073  qnegcl  13087  elpqb  13097  xrmax1  13298  xrmin2  13301  max1ALT  13309  xlesubadd  13386  xmulass  13410  xlemul1a  13411  xrsupexmnf  13428  xrinfmexpnf  13429  xrub  13435  iccid  13514  fzsn  13693  fzsuc2  13709  fz1sbc  13727  elfzp12  13730  modmuladd  14049  seqid3  14182  bcval5  14455  bcpasc  14458  hashbnd  14473  hashnnn0genn0  14480  hashprg  14532  hashfzo  14567  tpfo  14638  wrdl1s1  14755  ccats1alpha  14760  cats1un  14863  s7f1o  15112  shftlem  15214  replim  15276  absmod0  15463  absz  15471  rlimdm  15711  summolem2  15875  summo  15876  zsum  15877  fsum  15879  fsummulc2  15943  fsumconst  15949  fsum00  15958  incexclem  15998  isumsplit  16002  infcvgaux1i  16019  prodmolem2  16095  prodmo  16096  zprod  16097  fprod  16101  prodsn  16122  prodsnf  16124  fprodconst  16138  ruclem2  16393  fzo0dvdseq  16486  bitsf1ocnv  16607  sadcaddlem  16620  smueqlem  16653  gcdabs1  16695  bezoutlem1  16705  bezoutlem3  16707  bezoutlem4  16708  dvdsgcd  16710  dvdsmulgcd  16723  lcmgcdeq  16780  lcmf  16801  lcmfunsnlem1  16805  lcmfunsnlem2lem2  16807  isprm2lem  16849  dvdsprime  16855  isprm5  16876  coprm  16880  prmdvdsexpr  16886  rpexp  16891  phibndlem  16940  dfphi2  16944  hashgcdlem  16958  odzdvds  16966  nnoddn2prm  16982  pythagtriplem1  16987  iserodd  17006  pceulem  17016  pcqmul  17024  pcqcl  17027  pcxnn0cl  17031  pcxcl  17032  pcneg  17045  pcabs  17046  pcgcd1  17048  pcz  17052  pcprmpw2  17053  pcprmpw  17054  dvdsprmpweqle  17057  difsqpwdvds  17058  pcaddlem  17059  pcadd  17060  pcmpt  17063  pockthg  17077  prmreclem5  17091  4sqlem4  17123  mul4sq  17125  vdwapun  17145  vdwlem2  17153  vdwlem6  17157  vdwlem8  17159  vdwlem13  17164  0ram  17191  ram0  17193  ramcl  17200  cshwsiun  17270  wunress  17420  firest  17596  isssc  17988  pospo  18510  latnlej  18623  gsumval2a  18867  xpsmnd0  18965  mnd1id  18967  0subm  19006  mulgnn0p1  19288  mulgnn0ass  19313  cyccom  19411  gicsubgen  19486  symg1bas  19598  snsymgefmndeq  19602  psgnunilem1  19700  psgnunilem2  19702  mndodcongi  19750  oddvdsnn0  19751  odnncl  19752  oddvds  19754  odeq  19757  odeq1  19767  pgpfi2  19813  sylow2a  19826  sylow2blem3  19829  sylow3lem6  19839  lsmelvalm  19858  lsmsubm  19860  lsmsubg  19861  lsmmod  19882  lsmdisj2  19889  efgmnvl  19921  efgtlen  19933  efgs1b  19943  efgrelexlemb  19957  efgredeu  19959  efgcpbllemb  19962  frgpuptinv  19978  frgpup3lem  19984  qusabl  20072  frgpnabllem1  20080  cyggeninv  20090  cyggenod  20091  gsumval3eu  20111  dprdssv  20225  dprdfeq0  20231  dprdsubg  20233  dprddisj2  20248  ablfacrp  20275  pgpfac1lem3  20286  pgpfaclem2  20291  xpsring1d  20556  dvreq1  20634  irredn1  20649  crngrhmfo  20719  nzrunit  20768  ringcinv  20916  rrgeq0  20945  domneq0  20953  isdrng5  21001  isabvd  21062  abvdom  21080  issrngd  21105  lmodfopnelem2  21167  lss1d  21231  lspsneq0  21280  lbspss  21350  lsmcl  21351  lvecvs0or  21379  lspindpi  21403  lidl1el  21498  rspsn0  21519  lpiss  21646  lidldvgen  21651  qsssubdrg  21725  zringlpirlem1  21761  pzriprnglem6  21785  pzriprnglem12  21791  znfld  21859  znunit  21862  znrrg  21864  cygznlem3  21868  frgpcyg  21872  psgnghm  21879  ipeq0  21937  cssincl  21987  lsmcss  21991  obselocv  22027  dsmmacl  22040  dsmmlss  22043  lindsenlbs  22150  mplsubrglem  22304  mplmonmul  22338  mplcoe5lem  22341  mhpsclcl  22461  mhpvarcl  22462  psdmul  22480  coe1tmmul2  22588  coe1tmmul  22589  pf1ind  22666  mat1dimelbas  22779  mdetralt  22916  mdetunilem2  22921  mdetunilem7  22926  mdetunilem9  22928  maducoeval2  22948  chpscmat  23153  chfacfscmulgsum  23171  chfacfpmmulgsum  23175  istopon  23223  eltg3  23273  tgidm  23291  clsval2  23361  opncldf1  23395  restbas  23469  tgrest  23470  restcld  23483  restcldr  23485  restcls  23492  restntr  23493  ordtbas2  23502  ordtbas  23503  ordtrest2lem  23514  ordtrest2  23515  pnfnei  23531  mnfnei  23532  tgcn  23563  cnconst  23595  cnindis  23603  lmss  23609  ordtt1  23690  discmp  23709  1stcrest  23764  2ndcdisj  23768  cldllycmp  23807  txbas  23879  ptpjpre1  23883  ptuni2  23888  ptbasin  23889  ptbasfi  23893  ptopn2  23896  txbasval  23918  ptpjopn  23924  ptclsg  23927  dfac14lem  23929  xkoccn  23931  ptcnp  23934  upxp  23935  ptrescn  23951  txkgen  23964  xkoptsub  23966  xkopt  23967  xkoco1cn  23969  xkoco2cn  23970  xkococn  23972  xkoinjcn  23999  ordthmeolem  24113  ptuncnv  24119  nrmhaus  24138  fbssint  24150  fbfinnfr  24153  fbasrn  24196  isufil2  24220  filufint  24232  rnelfm  24265  fmfnfmlem2  24267  fmfnfmlem3  24268  fmfnfmlem4  24269  fmfnfm  24270  flimtopon  24282  flimclslem  24296  fclstopon  24324  fclscf  24337  flimfnfcls  24340  alexsublem  24356  alexsubALTlem3  24361  alexsubALTlem4  24362  ptcmplem2  24365  tmdgsum2  24408  symgtgp  24418  cldsubg  24423  qustgplem  24433  tgptsmscld  24463  tsmsxplem1  24465  imasdsf1olem  24685  blssps  24736  blss  24737  stdbdxmet  24827  methaus  24832  metrest  24836  nrginvrcn  25004  nmoeq0  25048  blssioo  25107  xrtgioo  25119  xrsxmet  25122  reconnlem1  25139  reconnlem2  25140  xrge0tsms  25147  elcncf1di  25209  iccpnfcnv  25258  evth  25273  lebnumlem1  25275  lebnumlem2  25276  lebnumlem3  25277  nmoleub3  25433  minveclem3b  25742  ivthlem2  25766  ivthlem3  25767  elovolm  25789  ovolmge0  25791  ovoliun  25819  ovolicc2lem3  25833  ovolicc2  25836  voliunlem3  25866  dyaddisj  25910  dyadmax  25912  opnmblALT  25917  ismbfd  25953  ismbf2d  25954  mbfimaopnlem  25969  mbfimaopn2  25971  i1fmullem  26008  i1fres  26019  itg1climres  26028  mbfi1fseqlem4  26032  itg2lcl  26041  itgsplitioo  26151  ellimc2  26190  rolle  26303  dvlip  26306  dvge0  26319  dvne0  26324  lhop1lem  26326  tdeglem4  26371  degltlem1  26383  deg1nn0clb  26401  deg1lt0  26402  dvdsq1p  26474  ply1rem  26477  fta1g  26481  elply2  26507  plyf  26509  ne0p  26518  plyeq0lem  26522  plypf1  26524  0dgrb  26558  coe1termlem  26570  dgrcolem2  26586  plymul0or  26592  plyrem  26619  fta1  26622  rnplynfin  26623  quotcan  26625  aalioulem3  26654  eff1olem  26869  lognegb  26911  eflogeq  26923  argregt0  26931  argrege0  26932  tanarg  26940  cxpexp  26989  cxpeq0  26999  mulcxp  27006  cxpeq  27078  atans2  27252  scvxcvx  27306  dmgmaddn0  27343  isppw2  27435  vmappw  27436  vmacl  27438  efvmacl  27440  isnsqf  27455  mumullem2  27500  sqff1o  27502  dvdsppwf1o  27506  ppiublem1  27522  vmalelog  27525  chtublem  27531  fsumvma  27533  perfectlem2  27550  perfect  27551  bposlem1  27604  lgsmod  27643  lgsne0  27655  lgsdirnn0  27664  lgsqr  27671  lgsdchr  27675  gausslemma2dlem1a  27685  gausslemma2dlem6  27692  lgseisenlem2  27696  lgsquadlem1  27700  lgsquadlem2  27701  2lgslem1b  27712  2sqlem2  27738  mul2sq  27739  2sqlem7  27744  dchrisum0fno1  27831  pntrsumbnd2  27887  ostthlem1  27947  ostth2lem2  27954  ostth3  27958  ostth  27959  nolesgn2ores  28022  nogesgn1ores  28024  nolt02o  28045  nogt01o  28046  nosupbnd2  28066  noinfbnd2lem1  28080  noetasuplem4  28086  noetainflem4  28090  maxs1  28119  mins2  28122  ltsne  28124  eqcuts3  28183  cuteq1  28196  madef  28215  ltslpss  28287  lrrecfr  28322  addsval  28341  addsproplem2  28349  addsuniflem  28380  addbdaylem  28396  negsid  28420  negsunif  28434  mulsproplem5  28499  mulsproplem6  28500  mulsproplem7  28501  mulsproplem8  28502  mulsproplem9  28503  lemulsd  28517  sltmuls1  28526  sltmuls2  28527  ltmuls2  28550  muls0ord  28564  precsexlem8  28593  precsexlem9  28594  precsexlem11  28596  elons2  28637  oncutlt  28643  bdayons  28655  onaddscl  28656  onmulscl  28657  nnsge1  28722  n0fincut  28734  n0subs  28742  dfnns2  28751  eucliddivs  28755  znegscl  28771  zaddscl  28773  zmulscld  28776  elzn0s  28777  eln0zs  28779  n0seo  28800  zseo  28801  bdaypw2n0bndlem  28842  bdaypw2n0bnd  28843  z12no  28855  z12addscl  28856  z12negscl  28857  z12shalf  28859  z12zsodd  28861  z12sge0  28862  z12bdaylem  28863  bdayfinlem  28865  recut  28873  elreno2  28874  remulscllem1  28879  colinearalg  29481  axpasch  29512  axlowdimlem16  29528  axlowdimlem17  29529  axlowdim  29532  axcontlem2  29536  axcontlem4  29538  axcontlem7  29541  lpvtx  29639  edglnl  29714  numedglnl  29715  usgredgop  29744  usgrexmplef  29833  uhgrspansubgrlem  29864  uhgrspan1  29877  nbusgredgeu0  29942  nb3grprlem2  29955  cusgrsize2inds  30027  vtxd0nedgb  30062  rusgrpropnb  30157  upgrwlkvtxedg  30218  wlkp1lem1  30245  wlkp1lem6  30250  wlkp1lem8  30252  usgr2wlkneq  30335  crctcshwlk  30404  crctcsh  30406  iswwlksnon  30435  wlkiswwlks1  30449  wwlksnextbi  30476  wwlksnextproplem2  30492  wspthsnonn0vne  30499  clwlkclwwlklem2  30584  clwwisshclwws  30599  erclwwlktr  30606  clwwlkel  30630  clwwlkext2edg  30640  erclwwlkntr  30655  clwlknf1oclwwlknlem2  30666  clwlknf1oclwwlknlem3  30667  clwlknf1oclwwlkn  30668  clwwlknonccat  30680  0wlkons1  30705  3wlkdlem6  30759  eupth2eucrct  30811  frgrwopreglem2  30907  2clwwlk2clwwlk  30944  wlkl0  30961  nvmul0or  31245  ipasslem5  31430  ipasslem11  31435  hvmul0or  31620  his6  31694  hhssnv  31859  ocsh  31878  ocin  31891  shsidmi  31979  chnlen0  32039  h1de2bi  32149  h1de2ctlem  32150  h1de2ci  32151  spansni  32152  3oalem1  32257  nmcexi  32621  atcveq0  32943  chcv1  32950  cdjreui  33027  cdj3lem2b  33032  xrge0tsmsd  33627  1fldgenq  33877  psrmonmul  34175  ccfldextdgrr  34297  ordtrest2NEWlem  34547  ordtrest2NEW  34548  xrge0iifcnv  34558  esumc  34676  esumpcvgval  34703  ballotlemfc0  35118  ballotlemfcc  35119  axprALT2  35723  fineqvnttrclse  35775  gblacfnacd  35864  vonf1oonfo  35877  onvfowev  35878  subfacp1lem4  35927  subfacp1lem5  35928  erdszelem8  35942  sconnpi1  35983  cvmsss2  36018  cvmlift2lem12  36058  satfv0  36102  satfv0fun  36115  satf00  36118  sat1el2xp  36123  fmla0xp  36127  fmlasucdisj  36143  satffunlem1lem1  36146  satffunlem2lem1  36148  dmopab3rexdif  36149  msubco  36275  msubvrs  36304  ellcsrspsn  36385  sinccvglem  36416  untsucf  36454  nnuni  36471  dfrdg2  36537  colineardim1  36806  btwnconn1lem14  36845  segleantisym  36860  colinbtwnle  36863  outsidele  36877  lineunray  36892  linethru  36898  nmulprop  36919  nmuladdss  36942  elicc3  37085  opnregcld  37098  cldregopn  37099  fnejoin2  37137  bj-isrvec  38195  dissneqlem  38243  icorempo  38254  relowlssretop  38266  relowlpssretop  38267  rdgssun  38281  finxpsuclem  38300  ptrecube  38518  poimirlem6  38524  poimirlem7  38525  poimirlem16  38534  poimirlem17  38535  poimirlem19  38537  poimirlem20  38538  poimirlem21  38539  poimirlem22  38540  poimirlem23  38541  poimirlem24  38542  poimirlem25  38543  poimirlem26  38544  poimirlem27  38545  poimirlem29  38547  poimirlem30  38548  poimirlem31  38549  poimirlem32  38550  itg2addnclem3  38571  ftc1anclem6  38596  dvasin  38602  unirep  38628  sdclem2  38656  ssbnd  38702  prdsbnd  38707  cntotbnd  38710  heibor1lem  38723  rrnequiv  38749  ismndo2  38788  grpoeqdivid  38795  isdrngo3  38873  crngohomfo  38920  0idl  38939  1idl  38940  divrngidl  38942  smprngopr  38966  prnc  38981  ispridlc  38984  disjimeceqim  39716  riotaclbgBAD  39991  lshpdisj  40024  lsateln0  40032  lsatcveq0  40069  opnlen0  40225  cmtbr4N  40292  cvrnbtwn2  40312  cvrnbtwn4  40316  atcvreq0  40351  cvlatexch1  40373  exatleN  40441  atlelt  40475  ps-2  40515  llnn0  40553  lplnn0N  40584  islpln2a  40585  lvoln0N  40628  islvol2aN  40629  4at  40650  dalemcea  40697  dalem3  40701  pmapglb2N  40808  pmapglb2xN  40809  cdlema1N  40828  cdlemb  40831  paddasslem17  40873  llnexchb2lem  40905  llnexchb2  40906  lhpat3  41083  ltrnid  41172  trlne  41222  cdlemc4  41231  cdleme11h  41303  cdlemednuN  41337  cdlemg1a  41607  tendoeq2  41811  tendoid0  41862  dva1dim  42022  dib1dim  42202  dihlatat  42374  dochkrshp4  42426  dochkr1  42515  lclkrlem2e  42548  lcfrlem16  42595  lcfrlem28  42607  mapd0  42702  hdmap14lem13  42917  eqresfnbd  43266  expeq1d  43361  expeqidd  43362  dvdsexpnn0  43366  reladdrsub  43416  sn-remul0ord  43439  sn-negex12  43448  sn-mullid  43467  sn-mul02  43496  nn0addcom  43506  nn0mulcom  43510  zmulcomlem  43511  mulgt0con1d  43514  mulgt0con2d  43515  sn-sup2  43535  frlmsnic  43584  evlselvlem  43596  prjspnnorm  43641  elrfi  43684  mrefg2  43697  eldiophb  43747  eldioph2b  43753  diophin  43762  diophun  43763  rexzrexnn0  43790  eldioph4b  43797  diophren  43799  rencldnfilem  43806  pellexlem6  43820  jm2.19  43979  rmydioph  44000  expdiophlem1  44007  expdioph  44009  lnr2i  44102  lpirlnr  44103  hbtlem2  44110  hbtlem4  44112  hbtlem6  44115  dgrsub2  44121  dgraa0p  44135  rngunsnply  44155  nlimsuc  44426  dfsucon  44508  radcnvrat  45283  pm14.24  45401  addrcom  45442  modelaxreplem1  45946  ormklocald  47855  afveu  48192  dfafn5b  48200  rlimdmafv  48216  afv2eu  48277  rlimdmafv2  48297  el1fzopredsuc  48365  minusmod5ne  48394  modmknepk  48407  elsetpreimafvssdm  48437  imasetpreimafvbijlemfo  48456  sprvalpw  48531  prprvalpw  48566  reupr  48573  fmtnofac2lem  48622  proththdlem  48667  perfectALTVlem2  48789  perfectALTV  48790  gbowpos  48826  gbowgt5  48829  gboge9  48831  nnsum4primesodd  48863  nnsum4primesoddALTV  48864  uhgrimedgi  48957  isuspgrim0  48961  isuspgrimlem  48962  upgrimpths  48976  clnbgrgrim  49001  grimedg  49002  grtrissvtx  49011  stgredgiun  49025  stgrvtx0  49029  isubgr3stgrlem7  49039  grlimgrtrilem2  49069  gpgiedgdmellem  49113  gpgvtxel2  49115  gpgvtx0  49120  gpgvtx1  49121  gpgusgralem  49123  gpgedgvtx0  49128  gpgedgvtx1  49129  gpgedg2ov  49133  gpgedg2iv  49134  gpgnbgrvtx0  49141  gpgnbgrvtx1  49142  pgnbgreunbgr  49192  ringcinvALTV  49376  smprngprmrng  49405  lincellss  49507  lindsrng01  49549  suppdm  49591  nnpw2pb  49668  0aryfvalel  49715  0aryfvalelfv  49716  itsclc0xyqsolr  49850  infsubc  50137  infsubc2  50138