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 ⊢ (𝜑 → (𝜒 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  biimprcd  253  iftrueb  4500  elsn2g  4630  preq1b  4811  elpreqprb  4833  reusv3  5376  alxfr  5378  reuhypd  5390  axpr  5398  opth1  5457  euotd  5496  otiunsndisj  5503  tz7.2  5644  frsn  5749  dmopab2rex  5907  elsnxp  6292  reuop  6294  dfpo2  6297  ordtri1  6394  ordtri3  6397  fvmptdv2  7008  fveqressseq  7074  foco2  7104  fsn  7131  fnsnbg  7162  fnsnbOLD  7164  fmptsng  7166  fmptsnd  7167  fconst2g  7201  fnprb  7206  fntpb  7207  funfvima  7228  soisoi  7326  isores3  7333  eqfunresadj  7358  riotaeqimp  7393  eusvobj2  7402  ovmpodv2  7568  f1opw2  7665  sorpssun  7727  sorpssin  7728  oneqmin  7795  nlimsucg  7834  onzsl  7838  tfinds  7852  funcnvuni  7925  mptcnfimad  7979  opiota  8052  mposn  8094  mpof1o2d  8117  frpoins3xpg  8132  frpoins3xp3g  8133  poxp2  8135  xpord2pred  8137  sexp2  8138  poxp3  8142  xpord3pred  8144  sexp3  8145  xpord3inddlem  8146  suppssov1  8189  suppssov2  8190  suppssfv  8194  brtpos  8227  frrlem12  8290  frrlem13  8291  seqomlem1  8433  seqomlem2  8434  omordi  8547  omord  8549  omwordi  8552  oeeui  8584  nnmordi  8613  nnmord  8614  nnmwordi  8617  nnawordex  8619  nnaordex  8620  nneob  8638  omsmolem  8639  eldifsucnn  8646  qsss  8769  eroveu  8806  mapsncnv  8887  ralxpmap  8890  elixpsn  8931  ixpsnf1o  8932  boxcutc  8935  pw2f1olem  9065  2pwne  9117  mapxpen  9127  mapunen  9130  php  9187  onomeneq  9194  unxpdomlem2  9213  en1eqsnbi  9232  isfiniteg  9256  fofinf1o  9285  f1opwfi  9309  elfiun  9386  oieu  9497  brwdom2  9531  wdomtr  9533  ixpiunwdom  9548  en3lplem1  9577  suc11reg  9584  inf3lemd  9592  cantnfvalf  9630  cantnflt  9637  cantnfp1lem3  9645  cantnflem2  9655  ttrcltr  9681  rnttrcl  9687  ttrclselem1  9690  r1tr  9744  updjud  9916  dfac8alem  10009  wdomnumr  10044  isinfcard  10072  aceq3lem  10100  dfac5lem4  10106  dfac5  10108  dfac2b  10110  coftr  10252  fin23lem28  10319  fin23lem29  10320  fin1a2lem11  10389  fin1a2lem12  10390  fin1a2lem13  10391  hsmexlem9  10404  axdclem  10498  pwcfsdom  10563  gchdomtri  10609  fpwwe2  10623  gchpwdom  10650  gchhar  10659  addnidpi  10881  nqereu  10909  genpv  10979  genpdm  10982  distrlem5pr  11007  mulrid  11201  ltne  11302  mul02  11383  cnegex  11386  mul0or  11849  negfi  12159  sup2  12166  supaddc  12177  supadd  12178  supmul1  12179  supmul  12182  creur  12207  creui  12208  cju  12209  nnsub  12275  un0addcl  12532  un0mulcl  12533  nn0sub  12549  elz2  12604  zaddcl  12629  suprzcl2  12957  qmulz  12970  qre  12972  qnegcl  12985  elpqb  12995  xrmax1  13196  xrmin2  13199  max1ALT  13207  xlesubadd  13284  xmulass  13308  xlemul1a  13309  xrsupexmnf  13326  xrinfmexpnf  13327  xrub  13333  iccid  13412  fzsn  13590  fzsuc2  13606  fz1sbc  13624  elfzp12  13627  modmuladd  13945  seqid3  14078  bcval5  14350  bcpasc  14353  hashbnd  14368  hashnnn0genn0  14375  hashprg  14427  hashfzo  14462  tpfo  14533  wrdl1s1  14648  ccats1alpha  14653  cats1un  14754  s7f1o  14999  shftlem  15101  replim  15163  absmod0  15350  absz  15358  rlimdm  15598  summolem2  15763  summo  15764  zsum  15765  fsum  15767  fsummulc2  15831  fsumconst  15837  fsum00  15846  incexclem  15886  isumsplit  15890  infcvgaux1i  15907  prodmolem2  15985  prodmo  15986  zprod  15987  fprod  15991  prodsn  16012  prodsnf  16014  fprodconst  16028  ruclem2  16283  fzo0dvdseq  16376  bitsf1ocnv  16497  sadcaddlem  16510  smueqlem  16543  gcdabs1  16582  bezoutlem1  16592  bezoutlem3  16594  bezoutlem4  16595  dvdsgcd  16597  dvdsmulgcd  16609  lcmgcdeq  16665  lcmf  16686  lcmfunsnlem1  16690  lcmfunsnlem2lem2  16692  isprm2lem  16734  dvdsprime  16740  isprm5  16761  coprm  16765  prmdvdsexpr  16771  rpexp  16776  phibndlem  16824  dfphi2  16828  hashgcdlem  16842  odzdvds  16850  nnoddn2prm  16866  pythagtriplem1  16871  iserodd  16890  pceulem  16900  pcqmul  16908  pcqcl  16911  pcxnn0cl  16915  pcxcl  16916  pcneg  16929  pcabs  16930  pcgcd1  16932  pcz  16936  pcprmpw2  16937  pcprmpw  16938  dvdsprmpweqle  16941  difsqpwdvds  16942  pcaddlem  16943  pcadd  16944  pcmpt  16947  pockthg  16961  prmreclem5  16975  4sqlem4  17007  mul4sq  17009  vdwapun  17029  vdwlem2  17037  vdwlem6  17041  vdwlem8  17043  vdwlem13  17048  0ram  17075  ram0  17077  ramcl  17084  cshwsiun  17154  wunress  17304  firest  17480  isssc  17872  pospo  18394  latnlej  18507  gsumval2a  18738  xpsmnd0  18831  mnd1id  18833  0subm  18871  mulgnn0p1  19146  mulgnn0ass  19171  cyccom  19269  gicsubgen  19344  symg1bas  19456  snsymgefmndeq  19460  psgnunilem1  19558  psgnunilem2  19560  mndodcongi  19608  oddvdsnn0  19609  odnncl  19610  oddvds  19612  odeq  19615  odeq1  19625  pgpfi2  19671  sylow2a  19684  sylow2blem3  19687  sylow3lem6  19697  lsmelvalm  19716  lsmsubm  19718  lsmsubg  19719  lsmmod  19740  lsmdisj2  19747  efgmnvl  19779  efgtlen  19791  efgs1b  19801  efgrelexlemb  19815  efgredeu  19817  efgcpbllemb  19820  frgpuptinv  19836  frgpup3lem  19842  qusabl  19930  frgpnabllem1  19938  cyggeninv  19948  cyggenod  19949  gsumval3eu  19969  dprdssv  20083  dprdfeq0  20089  dprdsubg  20091  dprddisj2  20106  ablfacrp  20133  pgpfac1lem3  20144  pgpfaclem2  20149  xpsring1d  20411  dvreq1  20489  irredn1  20504  crngrhmfo  20574  nzrunit  20622  ringcinv  20770  rrgeq0  20799  domneq0  20807  isdrng5  20854  isabvd  20915  abvdom  20933  issrngd  20958  lmodfopnelem2  21020  lss1d  21084  lspsneq0  21133  lbspss  21203  lsmcl  21204  lvecvs0or  21232  lspindpi  21256  lidl1el  21351  rspsn0  21372  lpiss  21497  lidldvgen  21502  qsssubdrg  21576  zringlpirlem1  21612  pzriprnglem6  21636  pzriprnglem12  21642  znfld  21710  znunit  21713  znrrg  21715  cygznlem3  21719  frgpcyg  21723  psgnghm  21730  ipeq0  21788  cssincl  21838  lsmcss  21842  obselocv  21878  dsmmacl  21891  dsmmlss  21894  mplsubrglem  22153  mplmonmul  22187  mplcoe5lem  22190  mhpsclcl  22310  mhpvarcl  22311  psdmul  22329  coe1tmmul2  22437  coe1tmmul  22438  pf1ind  22515  mat1dimelbas  22628  mdetralt  22765  mdetunilem2  22770  mdetunilem7  22775  mdetunilem9  22777  maducoeval2  22797  chpscmat  22999  chfacfscmulgsum  23017  chfacfpmmulgsum  23021  istopon  23069  eltg3  23119  tgidm  23137  clsval2  23207  opncldf1  23241  restbas  23315  tgrest  23316  restcld  23329  restcldr  23331  restcls  23338  restntr  23339  ordtbas2  23348  ordtbas  23349  ordtrest2lem  23360  ordtrest2  23361  pnfnei  23377  mnfnei  23378  tgcn  23409  cnconst  23441  cnindis  23449  lmss  23455  ordtt1  23536  discmp  23555  1stcrest  23610  2ndcdisj  23613  cldllycmp  23652  txbas  23724  ptpjpre1  23728  ptuni2  23733  ptbasin  23734  ptbasfi  23738  ptopn2  23741  txbasval  23763  ptpjopn  23769  ptclsg  23772  dfac14lem  23774  xkoccn  23776  ptcnp  23779  upxp  23780  ptrescn  23796  txkgen  23809  xkoptsub  23811  xkopt  23812  xkoco1cn  23814  xkoco2cn  23815  xkococn  23817  xkoinjcn  23844  ordthmeolem  23958  ptuncnv  23964  nrmhaus  23983  fbssint  23995  fbfinnfr  23998  fbasrn  24041  isufil2  24065  filufint  24077  rnelfm  24110  fmfnfmlem2  24112  fmfnfmlem3  24113  fmfnfmlem4  24114  fmfnfm  24115  flimtopon  24127  flimclslem  24141  fclstopon  24169  fclscf  24182  flimfnfcls  24185  alexsublem  24201  alexsubALTlem3  24206  alexsubALTlem4  24207  ptcmplem2  24210  tmdgsum2  24253  symgtgp  24263  cldsubg  24268  qustgplem  24278  tgptsmscld  24308  tsmsxplem1  24310  imasdsf1olem  24530  blssps  24581  blss  24582  stdbdxmet  24672  methaus  24677  metrest  24681  nrginvrcn  24849  nmoeq0  24893  blssioo  24952  xrtgioo  24964  xrsxmet  24967  reconnlem1  24984  reconnlem2  24985  xrge0tsms  24992  elcncf1di  25054  iccpnfcnv  25103  evth  25118  lebnumlem1  25120  lebnumlem2  25121  lebnumlem3  25122  nmoleub3  25278  minveclem3b  25587  ivthlem2  25611  ivthlem3  25612  elovolm  25634  ovolmge0  25636  ovoliun  25664  ovolicc2lem3  25678  ovolicc2  25681  voliunlem3  25711  dyaddisj  25755  dyadmax  25757  opnmblALT  25762  ismbfd  25798  ismbf2d  25799  mbfimaopnlem  25814  mbfimaopn2  25816  i1fmullem  25853  i1fres  25864  itg1climres  25873  mbfi1fseqlem4  25877  itg2lcl  25886  itgsplitioo  25997  ellimc2  26036  rolle  26149  dvlip  26152  dvge0  26165  dvne0  26170  lhop1lem  26172  tdeglem4  26217  degltlem1  26229  deg1nn0clb  26247  deg1lt0  26248  dvdsq1p  26320  ply1rem  26323  fta1g  26327  elply2  26353  plyf  26355  ne0p  26364  plyeq0lem  26367  plypf1  26369  0dgrb  26403  coe1termlem  26415  dgrcolem2  26431  plymul0or  26439  plyrem  26466  fta1  26469  quotcan  26470  aalioulem3  26497  eff1olem  26713  lognegb  26755  eflogeq  26767  argregt0  26775  argrege0  26776  tanarg  26784  cxpexp  26833  cxpeq0  26843  mulcxp  26850  cxpeq  26922  atans2  27096  scvxcvx  27150  dmgmaddn0  27187  isppw2  27279  vmappw  27280  vmacl  27282  efvmacl  27284  isnsqf  27299  mumullem2  27344  sqff1o  27346  dvdsppwf1o  27350  ppiublem1  27366  vmalelog  27369  chtublem  27375  fsumvma  27377  perfectlem2  27394  perfect  27395  bposlem1  27448  lgsmod  27487  lgsne0  27499  lgsdirnn0  27508  lgsqr  27515  lgsdchr  27519  gausslemma2dlem1a  27529  gausslemma2dlem6  27536  lgseisenlem2  27540  lgsquadlem1  27544  lgsquadlem2  27545  2lgslem1b  27556  2sqlem2  27582  mul2sq  27583  2sqlem7  27588  dchrisum0fno1  27675  pntrsumbnd2  27731  ostthlem1  27791  ostth2lem2  27798  ostth3  27802  ostth  27803  nolesgn2ores  27836  nogesgn1ores  27838  nolt02o  27859  nogt01o  27860  nosupbnd2  27880  noinfbnd2lem1  27894  noetasuplem4  27900  noetainflem4  27904  maxs1  27933  mins2  27936  ltsne  27938  eqcuts3  27997  cuteq1  28010  madef  28029  ltslpss  28101  lrrecfr  28136  addsval  28155  addsproplem2  28163  addsuniflem  28194  addbdaylem  28210  negsid  28234  negsunif  28248  mulsproplem5  28313  mulsproplem6  28314  mulsproplem7  28315  mulsproplem8  28316  mulsproplem9  28317  lemulsd  28331  sltmuls1  28340  sltmuls2  28341  ltmuls2  28364  muls0ord  28378  precsexlem8  28407  precsexlem9  28408  precsexlem11  28410  elons2  28451  oncutlt  28457  bdayons  28469  onaddscl  28470  onmulscl  28471  nnsge1  28536  n0fincut  28548  n0subs  28556  dfnns2  28565  eucliddivs  28569  znegscl  28585  zaddscl  28587  zmulscld  28590  elzn0s  28591  eln0zs  28593  n0seo  28614  zseo  28615  bdaypw2n0bndlem  28656  bdaypw2n0bnd  28657  z12no  28669  z12addscl  28670  z12negscl  28671  z12shalf  28673  z12zsodd  28675  z12sge0  28676  z12bdaylem  28677  bdayfinlem  28679  recut  28687  elreno2  28688  remulscllem1  28693  colinearalg  29260  axpasch  29291  axlowdimlem16  29307  axlowdimlem17  29308  axlowdim  29311  axcontlem2  29315  axcontlem4  29317  axcontlem7  29320  lpvtx  29418  edglnl  29493  numedglnl  29494  usgredgop  29520  usgrexmplef  29609  uhgrspansubgrlem  29640  uhgrspan1  29653  nbusgredgeu0  29718  nb3grprlem2  29731  cusgrsize2inds  29803  vtxd0nedgb  29838  rusgrpropnb  29933  upgrwlkvtxedg  29994  wlkp1lem1  30021  wlkp1lem6  30026  wlkp1lem8  30028  usgr2wlkneq  30105  crctcshwlk  30171  crctcsh  30173  iswwlksnon  30202  wlkiswwlks1  30216  wwlksnextbi  30243  wwlksnextproplem2  30259  wspthsnonn0vne  30266  clwlkclwwlklem2  30351  clwwisshclwws  30366  erclwwlktr  30373  clwwlkel  30397  clwwlkext2edg  30407  erclwwlkntr  30422  clwlknf1oclwwlknlem2  30433  clwlknf1oclwwlknlem3  30434  clwlknf1oclwwlkn  30435  clwwlknonccat  30447  0wlkons1  30472  3wlkdlem6  30516  eupth2eucrct  30568  frgrwopreglem2  30664  2clwwlk2clwwlk  30701  wlkl0  30718  nvmul0or  31002  ipasslem5  31187  ipasslem11  31192  hvmul0or  31377  his6  31451  hhssnv  31616  ocsh  31635  ocin  31648  shsidmi  31736  chnlen0  31796  h1de2bi  31906  h1de2ctlem  31907  h1de2ci  31908  spansni  31909  3oalem1  32014  nmcexi  32378  atcveq0  32700  chcv1  32707  cdjreui  32784  cdj3lem2b  32789  xrge0tsmsd  33393  1fldgenq  33643  psrmonmul  33940  ccfldextdgrr  34062  ordtrest2NEWlem  34312  ordtrest2NEW  34313  xrge0iifcnv  34323  esumc  34441  esumpcvgval  34468  ballotlemfc0  34883  ballotlemfcc  34884  fissorduni  35480  axprALT2  35503  fineqvnttrclse  35537  gblacfnacd  35586  vonf1oonfo  35599  onvfowev  35600  subfacp1lem4  35675  subfacp1lem5  35676  erdszelem8  35690  sconnpi1  35731  cvmsss2  35766  cvmlift2lem12  35806  satfv0  35850  satfv0fun  35863  satf00  35866  sat1el2xp  35871  fmla0xp  35875  fmlasucdisj  35891  satffunlem1lem1  35894  satffunlem2lem1  35896  dmopab3rexdif  35897  msubco  36023  msubvrs  36052  ellcsrspsn  36133  sinccvglem  36164  untsucf  36202  nnuni  36219  dfrdg2  36285  colineardim1  36553  btwnconn1lem14  36592  segleantisym  36607  colinbtwnle  36610  outsidele  36624  lineunray  36639  linethru  36645  nmulprop  36682  nmuladdss  36690  elicc3  36828  opnregcld  36841  cldregopn  36842  fnejoin2  36880  bj-isrvec  37938  dissneqlem  37986  icorempo  37997  relowlssretop  38009  relowlpssretop  38010  rdgssun  38024  finxpsuclem  38043  lindsenlbs  38266  ptrecube  38271  poimirlem6  38277  poimirlem7  38278  poimirlem16  38287  poimirlem17  38288  poimirlem19  38290  poimirlem20  38291  poimirlem21  38292  poimirlem22  38293  poimirlem23  38294  poimirlem24  38295  poimirlem25  38296  poimirlem26  38297  poimirlem27  38298  poimirlem29  38300  poimirlem30  38301  poimirlem31  38302  poimirlem32  38303  itg2addnclem3  38324  ftc1anclem6  38349  dvasin  38355  unirep  38365  sdclem2  38393  ssbnd  38439  prdsbnd  38444  cntotbnd  38447  heibor1lem  38460  rrnequiv  38486  ismndo2  38525  grpoeqdivid  38532  isdrngo3  38610  crngohomfo  38657  0idl  38676  1idl  38677  divrngidl  38679  smprngopr  38703  prnc  38718  ispridlc  38721  disjimeceqim  39453  riotaclbgBAD  39728  lshpdisj  39761  lsateln0  39769  lsatcveq0  39806  opnlen0  39962  cmtbr4N  40029  cvrnbtwn2  40049  cvrnbtwn4  40053  atcvreq0  40088  cvlatexch1  40110  exatleN  40178  atlelt  40212  ps-2  40252  llnn0  40290  lplnn0N  40321  islpln2a  40322  lvoln0N  40365  islvol2aN  40366  4at  40387  dalemcea  40434  dalem3  40438  pmapglb2N  40545  pmapglb2xN  40546  cdlema1N  40565  cdlemb  40568  paddasslem17  40610  llnexchb2lem  40642  llnexchb2  40643  lhpat3  40820  ltrnid  40909  trlne  40959  cdlemc4  40968  cdleme11h  41040  cdlemednuN  41074  cdlemg1a  41344  tendoeq2  41548  tendoid0  41599  dva1dim  41759  dib1dim  41939  dihlatat  42111  dochkrshp4  42163  dochkr1  42252  lclkrlem2e  42285  lcfrlem16  42332  lcfrlem28  42344  mapd0  42439  hdmap14lem13  42654  eqresfnbd  43003  expeq1d  43085  expeqidd  43086  dvdsexpnn0  43095  reladdrsub  43146  sn-remul0ord  43169  sn-negex12  43178  sn-mullid  43197  sn-mul02  43226  nn0addcom  43236  nn0mulcom  43240  zmulcomlem  43241  mulgt0con1d  43244  mulgt0con2d  43245  sn-sup2  43265  frlmsnic  43308  evlselvlem  43320  prjspner1  43358  elrfi  43425  mrefg2  43438  eldiophb  43488  eldioph2b  43494  diophin  43503  diophun  43504  rexzrexnn0  43531  eldioph4b  43538  diophren  43540  rencldnfilem  43547  pellexlem6  43561  jm2.19  43720  rmydioph  43741  expdiophlem1  43748  expdioph  43750  lnr2i  43843  lpirlnr  43844  hbtlem2  43851  hbtlem4  43853  hbtlem6  43856  dgrsub2  43862  dgraa0p  43876  rngunsnply  43896  nlimsuc  44167  dfsucon  44249  radcnvrat  45024  pm14.24  45142  addrcom  45183  modelaxreplem1  45687  ormklocald  47590  natlocalincr  47592  afveu  47890  dfafn5b  47898  rlimdmafv  47914  afv2eu  47975  rlimdmafv2  47995  el1fzopredsuc  48063  minusmod5ne  48092  modmknepk  48105  elsetpreimafvssdm  48135  imasetpreimafvbijlemfo  48154  sprvalpw  48229  prprvalpw  48264  reupr  48271  fmtnofac2lem  48320  proththdlem  48365  perfectALTVlem2  48487  perfectALTV  48488  gbowpos  48524  gbowgt5  48527  gboge9  48529  nnsum4primesodd  48561  nnsum4primesoddALTV  48562  uhgrimedgi  48655  isuspgrim0  48659  isuspgrimlem  48660  upgrimpths  48674  clnbgrgrim  48699  grimedg  48700  grtrissvtx  48709  stgredgiun  48723  stgrvtx0  48727  isubgr3stgrlem7  48737  grlimgrtrilem2  48767  gpgiedgdmellem  48811  gpgvtxel2  48813  gpgvtx0  48818  gpgvtx1  48819  gpgusgralem  48821  gpgedgvtx0  48826  gpgedgvtx1  48827  gpgedg2ov  48831  gpgedg2iv  48832  gpgnbgrvtx0  48839  gpgnbgrvtx1  48840  pgnbgreunbgr  48890  ringcinvALTV  49075  smprngprmrng  49104  lincellss  49206  lindsrng01  49248  suppdm  49290  nnpw2pb  49367  0aryfvalel  49414  0aryfvalelfv  49415  itsclc0xyqsolr  49549  infsubc  49838  infsubc2  49839