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  4505  elsn2g  4635  preq1b  4815  elpreqprb  4837  reusv3  5377  alxfr  5379  reuhypd  5391  axpr  5399  opth1  5458  euotd  5497  otiunsndisj  5504  tz7.2  5645  frsn  5750  dmopab2rex  5908  elsnxp  6293  reuop  6295  dfpo2  6298  ordtri1  6395  ordtri3  6398  fvmptdv2  7009  fveqressseq  7075  foco2  7105  fsn  7132  fnsnbg  7163  fnsnbOLD  7165  fmptsng  7167  fmptsnd  7168  fconst2g  7202  fnprb  7207  fntpb  7208  funfvima  7229  soisoi  7327  isores3  7334  eqfunresadj  7359  riotaeqimp  7394  eusvobj2  7403  ovmpodv2  7569  f1opw2  7666  sorpssun  7728  sorpssin  7729  oneqmin  7798  nlimsucg  7837  onzsl  7841  tfinds  7855  funcnvuni  7928  mptcnfimad  7982  opiota  8055  mposn  8097  mpof1o2d  8120  frpoins3xpg  8135  frpoins3xp3g  8136  poxp2  8138  xpord2pred  8140  sexp2  8141  poxp3  8145  xpord3pred  8147  sexp3  8148  xpord3inddlem  8149  suppssov1  8192  suppssov2  8193  suppssfv  8197  brtpos  8230  frrlem12  8293  frrlem13  8294  seqomlem1  8436  seqomlem2  8437  omordi  8550  omord  8552  omwordi  8555  oeeui  8587  nnmordi  8616  nnmord  8617  nnmwordi  8620  nnawordex  8622  nnaordex  8623  nneob  8641  omsmolem  8642  eldifsucnn  8649  qsss  8772  eroveu  8809  mapsncnv  8890  ralxpmap  8893  elixpsn  8934  ixpsnf1o  8935  boxcutc  8938  pw2f1olem  9068  2pwne  9120  mapxpen  9130  mapunen  9133  php  9190  onomeneq  9197  unxpdomlem2  9216  en1eqsnbi  9235  isfiniteg  9259  fofinf1o  9288  f1opwfi  9312  elfiun  9389  oieu  9500  brwdom2  9534  wdomtr  9536  ixpiunwdom  9551  en3lplem1  9580  suc11reg  9587  inf3lemd  9595  cantnfvalf  9633  cantnflt  9640  cantnfp1lem3  9648  cantnflem2  9658  ttrcltr  9684  rnttrcl  9690  ttrclselem1  9693  r1tr  9747  updjud  9919  dfac8alem  10012  wdomnumr  10047  isinfcard  10075  aceq3lem  10103  dfac5lem4  10109  dfac5  10111  dfac2b  10113  coftr  10256  fin23lem28  10323  fin23lem29  10324  fin1a2lem11  10393  fin1a2lem12  10394  fin1a2lem13  10395  hsmexlem9  10408  axdclem  10502  pwcfsdom  10567  gchdomtri  10613  fpwwe2  10627  gchpwdom  10654  gchhar  10663  addnidpi  10885  nqereu  10913  genpv  10983  genpdm  10986  distrlem5pr  11011  mulrid  11205  ltne  11306  mul02  11387  cnegex  11390  mul0or  11853  negfi  12163  sup2  12170  supaddc  12181  supadd  12182  supmul1  12183  supmul  12186  creur  12211  creui  12212  cju  12213  nnsub  12279  un0addcl  12536  un0mulcl  12537  nn0sub  12553  elz2  12608  zaddcl  12633  suprzcl2  12961  qmulz  12974  qre  12976  qnegcl  12989  elpqb  12999  xrmax1  13200  xrmin2  13203  max1ALT  13211  xlesubadd  13288  xmulass  13312  xlemul1a  13313  xrsupexmnf  13330  xrinfmexpnf  13331  xrub  13337  iccid  13416  fzsn  13593  fzsuc2  13609  fz1sbc  13627  elfzp12  13630  modmuladd  13948  seqid3  14081  bcval5  14353  bcpasc  14356  hashbnd  14371  hashnnn0genn0  14378  hashprg  14430  hashfzo  14465  tpfo  14536  wrdl1s1  14651  ccats1alpha  14656  cats1un  14757  s7f1o  15002  shftlem  15104  replim  15166  absmod0  15353  absz  15361  rlimdm  15601  summolem2  15766  summo  15767  zsum  15768  fsum  15770  fsummulc2  15834  fsumconst  15840  fsum00  15849  incexclem  15889  isumsplit  15893  infcvgaux1i  15910  prodmolem2  15988  prodmo  15989  zprod  15990  fprod  15994  prodsn  16015  prodsnf  16017  fprodconst  16031  ruclem2  16287  fzo0dvdseq  16380  bitsf1ocnv  16501  sadcaddlem  16514  smueqlem  16547  gcdabs1  16586  bezoutlem1  16596  bezoutlem3  16598  bezoutlem4  16599  dvdsgcd  16601  dvdsmulgcd  16613  lcmgcdeq  16669  lcmf  16690  lcmfunsnlem1  16694  lcmfunsnlem2lem2  16696  isprm2lem  16738  dvdsprime  16744  isprm5  16765  coprm  16769  prmdvdsexpr  16775  rpexp  16780  phibndlem  16828  dfphi2  16832  hashgcdlem  16846  odzdvds  16854  nnoddn2prm  16870  pythagtriplem1  16875  iserodd  16894  pceulem  16904  pcqmul  16912  pcqcl  16915  pcxnn0cl  16919  pcxcl  16920  pcneg  16933  pcabs  16934  pcgcd1  16936  pcz  16940  pcprmpw2  16941  pcprmpw  16942  dvdsprmpweqle  16945  difsqpwdvds  16946  pcaddlem  16947  pcadd  16948  pcmpt  16951  pockthg  16965  prmreclem5  16979  4sqlem4  17011  mul4sq  17013  vdwapun  17033  vdwlem2  17041  vdwlem6  17045  vdwlem8  17047  vdwlem13  17052  0ram  17079  ram0  17081  ramcl  17088  cshwsiun  17158  wunress  17308  firest  17484  isssc  17876  pospo  18398  latnlej  18511  gsumval2a  18742  xpsmnd0  18835  mnd1id  18837  0subm  18875  mulgnn0p1  19150  mulgnn0ass  19175  cyccom  19273  gicsubgen  19348  symg1bas  19460  snsymgefmndeq  19464  psgnunilem1  19562  psgnunilem2  19564  mndodcongi  19612  oddvdsnn0  19613  odnncl  19614  oddvds  19616  odeq  19619  odeq1  19629  pgpfi2  19675  sylow2a  19688  sylow2blem3  19691  sylow3lem6  19701  lsmelvalm  19720  lsmsubm  19722  lsmsubg  19723  lsmmod  19744  lsmdisj2  19751  efgmnvl  19783  efgtlen  19795  efgs1b  19805  efgrelexlemb  19819  efgredeu  19821  efgcpbllemb  19824  frgpuptinv  19840  frgpup3lem  19846  qusabl  19934  frgpnabllem1  19942  cyggeninv  19952  cyggenod  19953  gsumval3eu  19973  dprdssv  20087  dprdfeq0  20093  dprdsubg  20095  dprddisj2  20110  ablfacrp  20137  pgpfac1lem3  20148  pgpfaclem2  20153  xpsring1d  20414  dvreq1  20492  irredn1  20507  nzrunit  20607  ringcinv  20755  rrgeq0  20784  domneq0  20792  isabvd  20892  abvdom  20910  issrngd  20935  lmodfopnelem2  20997  lss1d  21061  lspsneq0  21110  lbspss  21180  lsmcl  21181  lvecvs0or  21209  lspindpi  21233  lidl1el  21328  lpiss  21465  lidldvgen  21470  qsssubdrg  21544  zringlpirlem1  21580  pzriprnglem6  21604  pzriprnglem12  21610  znfld  21678  znunit  21681  znrrg  21683  cygznlem3  21687  frgpcyg  21691  psgnghm  21698  ipeq0  21756  cssincl  21806  lsmcss  21810  obselocv  21846  dsmmacl  21859  dsmmlss  21862  mplsubrglem  22121  mplmonmul  22155  mplcoe5lem  22158  mhpsclcl  22278  mhpvarcl  22279  psdmul  22297  coe1tmmul2  22405  coe1tmmul  22406  pf1ind  22483  mat1dimelbas  22596  mdetralt  22733  mdetunilem2  22738  mdetunilem7  22743  mdetunilem9  22745  maducoeval2  22765  chpscmat  22967  chfacfscmulgsum  22985  chfacfpmmulgsum  22989  istopon  23037  eltg3  23087  tgidm  23105  clsval2  23175  opncldf1  23209  restbas  23283  tgrest  23284  restcld  23297  restcldr  23299  restcls  23306  restntr  23307  ordtbas2  23316  ordtbas  23317  ordtrest2lem  23328  ordtrest2  23329  pnfnei  23345  mnfnei  23346  tgcn  23377  cnconst  23409  cnindis  23417  lmss  23423  ordtt1  23504  discmp  23523  1stcrest  23578  2ndcdisj  23581  cldllycmp  23620  txbas  23692  ptpjpre1  23696  ptuni2  23701  ptbasin  23702  ptbasfi  23706  ptopn2  23709  txbasval  23731  ptpjopn  23737  ptclsg  23740  dfac14lem  23742  xkoccn  23744  ptcnp  23747  upxp  23748  ptrescn  23764  txkgen  23777  xkoptsub  23779  xkopt  23780  xkoco1cn  23782  xkoco2cn  23783  xkococn  23785  xkoinjcn  23812  ordthmeolem  23926  ptuncnv  23932  nrmhaus  23951  fbssint  23963  fbfinnfr  23966  fbasrn  24009  isufil2  24033  filufint  24045  rnelfm  24078  fmfnfmlem2  24080  fmfnfmlem3  24081  fmfnfmlem4  24082  fmfnfm  24083  flimtopon  24095  flimclslem  24109  fclstopon  24137  fclscf  24150  flimfnfcls  24153  alexsublem  24169  alexsubALTlem3  24174  alexsubALTlem4  24175  ptcmplem2  24178  tmdgsum2  24221  symgtgp  24231  cldsubg  24236  qustgplem  24246  tgptsmscld  24276  tsmsxplem1  24278  imasdsf1olem  24498  blssps  24549  blss  24550  stdbdxmet  24640  methaus  24645  metrest  24649  nrginvrcn  24817  nmoeq0  24861  blssioo  24920  xrtgioo  24932  xrsxmet  24935  reconnlem1  24952  reconnlem2  24953  xrge0tsms  24960  elcncf1di  25022  iccpnfcnv  25071  evth  25086  lebnumlem1  25088  lebnumlem2  25089  lebnumlem3  25090  nmoleub3  25246  minveclem3b  25555  ivthlem2  25579  ivthlem3  25580  elovolm  25602  ovolmge0  25604  ovoliun  25632  ovolicc2lem3  25646  ovolicc2  25649  voliunlem3  25679  dyaddisj  25723  dyadmax  25725  opnmblALT  25730  ismbfd  25766  ismbf2d  25767  mbfimaopnlem  25782  mbfimaopn2  25784  i1fmullem  25821  i1fres  25832  itg1climres  25841  mbfi1fseqlem4  25845  itg2lcl  25854  itgsplitioo  25965  ellimc2  26004  rolle  26117  dvlip  26120  dvge0  26133  dvne0  26138  lhop1lem  26140  tdeglem4  26185  degltlem1  26197  deg1nn0clb  26215  deg1lt0  26216  dvdsq1p  26288  ply1rem  26291  fta1g  26295  elply2  26321  plyf  26323  ne0p  26332  plyeq0lem  26335  plypf1  26337  0dgrb  26371  coe1termlem  26383  dgrcolem2  26399  plymul0or  26407  plyrem  26434  fta1  26437  quotcan  26438  aalioulem3  26463  eff1olem  26678  lognegb  26720  eflogeq  26732  argregt0  26740  argrege0  26741  tanarg  26749  cxpexp  26798  cxpeq0  26808  mulcxp  26815  cxpeq  26887  atans2  27061  scvxcvx  27115  dmgmaddn0  27152  isppw2  27244  vmappw  27245  vmacl  27247  efvmacl  27249  isnsqf  27264  mumullem2  27309  sqff1o  27311  dvdsppwf1o  27315  ppiublem1  27331  vmalelog  27334  chtublem  27340  fsumvma  27342  perfectlem2  27359  perfect  27360  bposlem1  27413  lgsmod  27452  lgsne0  27464  lgsdirnn0  27473  lgsqr  27480  lgsdchr  27484  gausslemma2dlem1a  27494  gausslemma2dlem6  27501  lgseisenlem2  27505  lgsquadlem1  27509  lgsquadlem2  27510  2lgslem1b  27521  2sqlem2  27547  mul2sq  27548  2sqlem7  27553  dchrisum0fno1  27640  pntrsumbnd2  27696  ostthlem1  27756  ostth2lem2  27763  ostth3  27767  ostth  27768  nolesgn2ores  27801  nogesgn1ores  27803  nolt02o  27824  nogt01o  27825  nosupbnd2  27845  noinfbnd2lem1  27859  noetasuplem4  27865  noetainflem4  27869  maxs1  27898  mins2  27901  ltsne  27903  eqcuts3  27962  cuteq1  27975  madef  27994  ltslpss  28066  lrrecfr  28101  addsval  28120  addsproplem2  28128  addsuniflem  28159  addbdaylem  28175  negsid  28199  negsunif  28213  mulsproplem5  28278  mulsproplem6  28279  mulsproplem7  28280  mulsproplem8  28281  mulsproplem9  28282  lemulsd  28296  sltmuls1  28305  sltmuls2  28306  ltmuls2  28329  muls0ord  28343  precsexlem8  28372  precsexlem9  28373  precsexlem11  28375  elons2  28416  oncutlt  28422  bdayons  28434  onaddscl  28435  onmulscl  28436  nnsge1  28501  n0fincut  28513  n0subs  28521  dfnns2  28530  eucliddivs  28534  znegscl  28550  zaddscl  28552  zmulscld  28555  elzn0s  28556  eln0zs  28558  n0seo  28579  zseo  28580  bdaypw2n0bndlem  28621  bdaypw2n0bnd  28622  z12no  28634  z12addscl  28635  z12negscl  28636  z12shalf  28638  z12zsodd  28640  z12sge0  28641  z12bdaylem  28642  bdayfinlem  28644  recut  28652  elreno2  28653  remulscllem1  28658  colinearalg  29200  axpasch  29231  axlowdimlem16  29247  axlowdimlem17  29248  axlowdim  29251  axcontlem2  29255  axcontlem4  29257  axcontlem7  29260  lpvtx  29358  edglnl  29433  numedglnl  29434  usgredgop  29460  usgrexmplef  29549  uhgrspansubgrlem  29580  uhgrspan1  29593  nbusgredgeu0  29658  nb3grprlem2  29671  cusgrsize2inds  29743  vtxd0nedgb  29778  rusgrpropnb  29873  upgrwlkvtxedg  29934  wlkp1lem1  29961  wlkp1lem6  29966  wlkp1lem8  29968  usgr2wlkneq  30045  crctcshwlk  30111  crctcsh  30113  iswwlksnon  30142  wlkiswwlks1  30156  wwlksnextbi  30183  wwlksnextproplem2  30199  wspthsnonn0vne  30206  clwlkclwwlklem2  30291  clwwisshclwws  30306  erclwwlktr  30313  clwwlkel  30337  clwwlkext2edg  30347  erclwwlkntr  30362  clwlknf1oclwwlknlem2  30373  clwlknf1oclwwlknlem3  30374  clwlknf1oclwwlkn  30375  clwwlknonccat  30387  0wlkons1  30412  3wlkdlem6  30456  eupth2eucrct  30508  frgrwopreglem2  30604  2clwwlk2clwwlk  30641  wlkl0  30658  nvmul0or  30942  ipasslem5  31127  ipasslem11  31132  hvmul0or  31317  his6  31391  hhssnv  31556  ocsh  31575  ocin  31588  shsidmi  31676  chnlen0  31736  h1de2bi  31846  h1de2ctlem  31847  h1de2ci  31848  spansni  31849  3oalem1  31954  nmcexi  32318  atcveq0  32640  chcv1  32647  cdjreui  32724  cdj3lem2b  32729  xrge0tsmsd  33333  1fldgenq  33585  psrmonmul  33884  ccfldextdgrr  34006  ordtrest2NEWlem  34256  ordtrest2NEW  34257  xrge0iifcnv  34267  esumc  34385  esumpcvgval  34412  ballotlemfc0  34827  ballotlemfcc  34828  fissorduni  35422  axprALT2  35444  fineqvnttrclse  35459  gblacfnacd  35484  vonf1oonfo  35497  onvfowev  35498  subfacp1lem4  35573  subfacp1lem5  35574  erdszelem8  35588  sconnpi1  35629  cvmsss2  35664  cvmlift2lem12  35704  satfv0  35748  satfv0fun  35761  satf00  35764  sat1el2xp  35769  fmla0xp  35773  fmlasucdisj  35789  satffunlem1lem1  35792  satffunlem2lem1  35794  dmopab3rexdif  35795  msubco  35921  msubvrs  35950  ellcsrspsn  36031  sinccvglem  36062  untsucf  36100  nnuni  36117  dfrdg2  36183  colineardim1  36451  btwnconn1lem14  36490  segleantisym  36505  colinbtwnle  36508  outsidele  36522  lineunray  36537  linethru  36543  nmulprop  36580  elicc3  36716  opnregcld  36729  cldregopn  36730  fnejoin2  36768  bj-isrvec  37825  dissneqlem  37873  icorempo  37884  relowlssretop  37896  relowlpssretop  37897  rdgssun  37911  finxpsuclem  37930  lindsenlbs  38153  ptrecube  38158  poimirlem6  38164  poimirlem7  38165  poimirlem16  38174  poimirlem17  38175  poimirlem19  38177  poimirlem20  38178  poimirlem21  38179  poimirlem22  38180  poimirlem23  38181  poimirlem24  38182  poimirlem25  38183  poimirlem26  38184  poimirlem27  38185  poimirlem29  38187  poimirlem30  38188  poimirlem31  38189  poimirlem32  38190  itg2addnclem3  38211  ftc1anclem6  38236  dvasin  38242  unirep  38252  sdclem2  38280  ssbnd  38326  prdsbnd  38331  cntotbnd  38334  heibor1lem  38347  rrnequiv  38373  ismndo2  38412  grpoeqdivid  38419  isdrngo3  38497  crngohomfo  38544  0idl  38563  1idl  38564  divrngidl  38566  smprngopr  38590  prnc  38605  ispridlc  38608  disjimeceqim  39342  riotaclbgBAD  39617  lshpdisj  39650  lsateln0  39658  lsatcveq0  39695  opnlen0  39851  cmtbr4N  39918  cvrnbtwn2  39938  cvrnbtwn4  39942  atcvreq0  39977  cvlatexch1  39999  exatleN  40067  atlelt  40101  ps-2  40141  llnn0  40179  lplnn0N  40210  islpln2a  40211  lvoln0N  40254  islvol2aN  40255  4at  40276  dalemcea  40323  dalem3  40327  pmapglb2N  40434  pmapglb2xN  40435  cdlema1N  40454  cdlemb  40457  paddasslem17  40499  llnexchb2lem  40531  llnexchb2  40532  lhpat3  40709  ltrnid  40798  trlne  40848  cdlemc4  40857  cdleme11h  40929  cdlemednuN  40963  cdlemg1a  41233  tendoeq2  41437  tendoid0  41488  dva1dim  41648  dib1dim  41828  dihlatat  42000  dochkrshp4  42052  dochkr1  42141  lclkrlem2e  42174  lcfrlem16  42221  lcfrlem28  42233  mapd0  42328  hdmap14lem13  42543  eqresfnbd  42892  expeq1d  42974  expeqidd  42975  dvdsexpnn0  42984  reladdrsub  43035  sn-remul0ord  43058  sn-negex12  43067  sn-mullid  43086  sn-mul02  43115  nn0addcom  43125  nn0mulcom  43129  zmulcomlem  43130  mulgt0con1d  43133  mulgt0con2d  43134  sn-sup2  43154  frlmsnic  43199  evlselvlem  43211  prjspner1  43249  elrfi  43316  mrefg2  43329  eldiophb  43379  eldioph2b  43385  diophin  43394  diophun  43395  rexzrexnn0  43422  eldioph4b  43429  diophren  43431  rencldnfilem  43438  pellexlem6  43452  jm2.19  43611  rmydioph  43632  expdiophlem1  43639  expdioph  43641  lnr2i  43734  lpirlnr  43735  hbtlem2  43742  hbtlem4  43744  hbtlem6  43747  dgrsub2  43753  dgraa0p  43767  rngunsnply  43787  nlimsuc  44058  dfsucon  44140  radcnvrat  44915  pm14.24  45033  addrcom  45074  modelaxreplem1  45578  ormklocald  47481  natlocalincr  47483  afveu  47778  dfafn5b  47786  rlimdmafv  47802  afv2eu  47863  rlimdmafv2  47883  el1fzopredsuc  47951  minusmod5ne  47980  modmknepk  47993  elsetpreimafvssdm  48023  imasetpreimafvbijlemfo  48042  sprvalpw  48117  prprvalpw  48152  reupr  48159  fmtnofac2lem  48208  proththdlem  48253  perfectALTVlem2  48375  perfectALTV  48376  gbowpos  48412  gbowgt5  48415  gboge9  48417  nnsum4primesodd  48449  nnsum4primesoddALTV  48450  uhgrimedgi  48543  isuspgrim0  48547  isuspgrimlem  48548  upgrimpths  48562  clnbgrgrim  48587  grimedg  48588  grtrissvtx  48597  stgredgiun  48611  stgrvtx0  48615  isubgr3stgrlem7  48625  grlimgrtrilem2  48655  gpgiedgdmellem  48699  gpgvtxel2  48701  gpgvtx0  48706  gpgvtx1  48707  gpgusgralem  48709  gpgedgvtx0  48714  gpgedgvtx1  48715  gpgedg2ov  48719  gpgedg2iv  48720  gpgnbgrvtx0  48727  gpgnbgrvtx1  48728  pgnbgreunbgr  48778  ringcinvALTV  48963  smprngprmrng  48992  lincellss  49090  lindsrng01  49132  suppdm  49174  nnpw2pb  49251  0aryfvalel  49298  0aryfvalelfv  49299  itsclc0xyqsolr  49433  infsubc  49722  infsubc2  49723