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  4498  elsn2g  4626  preq1b  4806  elpreqprb  4828  reusv3  5374  alxfr  5376  reuhypd  5388  axpr  5396  opth1  5451  euotd  5493  otiunsndisj  5500  tz7.2  5641  frsn  5747  dmopab2rex  5911  idresdmsscocnv1  6281  elsnxp  6320  reuop  6322  dfpo2  6325  ordtri1  6422  ordtri3  6425  fvmptdv2  7043  fveqressseq  7111  foco2  7141  fsn  7168  fnsnbg  7201  fmptsng  7204  fmptsnd  7205  fconst2g  7240  fnprb  7245  fntpb  7246  funfvima  7267  soisoi  7367  isores3  7374  eqfunresadj  7401  riotaeqimp  7434  eusvobj2  7443  ovmpodv2  7610  f1opw2  7708  sorpssun  7778  sorpssin  7779  oneqmin  7848  nlimsucg  7887  onzsl  7891  tfinds  7905  funcnvuni  7978  mptcnfimad  8032  opiota  8105  mposn  8151  mpof1o2d  8174  frpoins3xpg  8194  frpoins3xp3g  8195  poxp2  8197  xpord2pred  8199  sexp2  8200  poxp3  8204  xpord3pred  8206  sexp3  8207  xpord3inddlem  8208  suppssov1  8252  suppssov2  8253  suppssfv  8257  brtpos  8290  frrlem12  8353  frrlem13  8354  seqomlem1  8498  seqomlem2  8499  omordi  8612  omord  8614  omwordi  8617  oeeui  8649  nnmordi  8678  nnmord  8679  nnmwordi  8682  nnawordex  8684  nnaordex  8685  nneob  8703  omsmolem  8704  eldifsucnn  8711  qsss  8834  eroveu  8871  mapsncnv  8959  ralxpmap  8962  elixpsn  9003  ixpsnf1o  9004  boxcutc  9007  pw2f1olem  9138  2pwne  9190  mapxpen  9200  mapunen  9203  php  9260  onomeneq  9267  unxpdomlem2  9286  en1eqsnbi  9305  fissorduni  9320  isfiniteg  9330  fofinf1o  9359  f1opwfi  9383  elfiun  9459  oieu  9570  brwdom2  9604  wdomtr  9606  ixpiunwdom  9621  en3lplem1  9650  suc11reg  9657  inf3lemd  9665  cantnfvalf  9703  cantnflt  9710  cantnfp1lem3  9718  cantnflem2  9728  ttrcltr  9754  rnttrcl  9760  ttrclselem1  9763  r1tr  9820  updjud  10052  dfac8alem  10147  wdomnumr  10182  isinfcard  10210  aceq3lem  10238  dfac5lem4  10244  dfac5  10246  dfac2b  10248  coftr  10390  fin23lem28  10457  fin23lem29  10458  fin1a2lem11  10527  fin1a2lem12  10528  fin1a2lem13  10529  hsmexlem9  10542  axdclem  10636  pwcfsdom  10707  gchdomtri  10753  fpwwe2  10767  gchpwdom  10794  gchhar  10803  addnidpi  11025  nqereu  11053  genpv  11123  genpdm  11126  distrlem5pr  11151  mulrid  11345  ltne  11446  mul02  11527  cnegex  11530  mul0or  11996  negfi  12306  sup2  12313  supaddc  12324  supadd  12325  supmul1  12326  supmul  12329  creur  12354  creui  12355  cju  12356  nnsub  12422  un0addcl  12679  un0mulcl  12680  nn0sub  12696  elz2  12751  zaddcl  12776  suprzcl2  13105  qmulz  13118  qre  13120  qnegcl  13134  elpqb  13144  xrmax1  13345  xrmin2  13348  max1ALT  13356  xlesubadd  13433  xmulass  13457  xlemul1a  13458  xrsupexmnf  13475  xrinfmexpnf  13476  xrub  13482  iccid  13561  fzsn  13740  fzsuc2  13756  fz1sbc  13774  elfzp12  13777  modmuladd  14096  seqid3  14229  bcval5  14503  bcpasc  14506  hashbnd  14521  hashnnn0genn0  14528  hashprg  14580  hashfzo  14615  tpfo  14686  wrdl1s1  14804  ccats1alpha  14809  cats1un  14912  s7f1o  15162  shftlem  15264  replim  15326  absmod0  15513  absz  15521  rlimdm  15762  summolem2  15926  summo  15927  zsum  15928  fsum  15930  fsummulc2  15994  fsumconst  16000  fsum00  16009  incexclem  16049  isumsplit  16053  infcvgaux1i  16070  prodmolem2  16146  prodmo  16147  zprod  16148  fprod  16152  prodsn  16173  prodsnf  16175  fprodconst  16189  ruclem2  16444  fzo0dvdseq  16537  bitsf1ocnv  16658  sadcaddlem  16671  smueqlem  16704  gcdabs1  16746  bezoutlem1  16756  bezoutlem3  16758  bezoutlem4  16759  dvdsgcd  16761  dvdsmulgcd  16774  lcmgcdeq  16831  lcmf  16852  lcmfunsnlem1  16856  lcmfunsnlem2lem2  16858  isprm2lem  16900  dvdsprime  16906  isprm5  16927  coprm  16931  prmdvdsexpr  16937  rpexp  16942  phibndlem  16991  dfphi2  16995  hashgcdlem  17009  odzdvds  17017  nnoddn2prm  17033  pythagtriplem1  17038  iserodd  17057  pceulem  17067  pcqmul  17075  pcqcl  17078  pcxnn0cl  17082  pcxcl  17083  pcneg  17096  pcabs  17097  pcgcd1  17099  pcz  17103  pcprmpw2  17104  pcprmpw  17105  dvdsprmpweqle  17108  difsqpwdvds  17109  pcaddlem  17110  pcadd  17111  pcmpt  17114  pockthg  17128  prmreclem5  17142  4sqlem4  17174  mul4sq  17176  vdwapun  17196  vdwlem2  17204  vdwlem6  17208  vdwlem8  17210  vdwlem13  17215  0ram  17242  ram0  17244  ramcl  17251  cshwsiun  17321  wunress  17471  firest  17653  isssc  18045  pospo  18567  latnlej  18680  gsumval2a  18924  xpsmnd0  19022  mnd1id  19024  0subm  19063  mulgnn0p1  19345  mulgnn0ass  19370  cyccom  19468  gicsubgen  19544  symg1bas  19656  snsymgefmndeq  19660  psgnunilem1  19758  psgnunilem2  19760  mndodcongi  19808  oddvdsnn0  19809  odnncl  19810  oddvds  19812  odeq  19815  odeq1  19825  pgpfi2  19871  sylow2a  19884  sylow2blem3  19887  sylow3lem6  19897  lsmelvalm  19916  lsmsubm  19918  lsmsubg  19919  lsmmod  19940  lsmdisj2  19947  efgmnvl  19979  efgtlen  19991  efgs1b  20001  efgrelexlemb  20015  efgredeu  20017  efgcpbllemb  20020  frgpuptinv  20036  frgpup3lem  20042  qusabl  20130  frgpnabllem1  20138  cyggeninv  20148  cyggenod  20149  gsumval3eu  20169  dprdssv  20283  dprdfeq0  20289  dprdsubg  20291  dprddisj2  20306  ablfacrp  20333  pgpfac1lem3  20344  pgpfaclem2  20349  xpsring1d  20614  dvreq1  20692  irredn1  20707  crngrhmfo  20777  nzrunit  20826  ringcinv  20974  rrgeq0  21003  domneq0  21011  isdrng5  21059  isabvd  21120  abvdom  21138  issrngd  21163  lmodfopnelem2  21225  lss1d  21289  lspsneq0  21338  lbspss  21408  lsmcl  21409  lvecvs0or  21437  lspindpi  21461  lidl1el  21556  rspsn0  21577  lpiss  21704  lidldvgen  21709  qsssubdrg  21786  zringlpirlem1  21823  pzriprnglem6  21847  pzriprnglem12  21853  znfld  21921  znunit  21924  znrrg  21926  cygznlem3  21930  frgpcyg  21934  psgnghm  21941  ipeq0  21999  cssincl  22049  lsmcss  22053  obselocv  22089  dsmmacl  22102  dsmmlss  22105  lindsenlbs  22212  mplsubrglem  22366  mplmonmul  22400  mplcoe5lem  22403  mhpsclcl  22523  mhpvarcl  22524  psdmul  22542  coe1tmmul2  22650  coe1tmmul  22651  pf1ind  22728  mat1dimelbas  22841  mdetralt  22978  mdetunilem2  22983  mdetunilem7  22988  mdetunilem9  22990  maducoeval2  23010  chpscmat  23215  chfacfscmulgsum  23233  chfacfpmmulgsum  23237  istopon  23285  eltg3  23335  tgidm  23353  clsval2  23423  opncldf1  23457  restbas  23531  tgrest  23532  restcld  23545  restcldr  23547  restcls  23554  restntr  23555  ordtbas2  23564  ordtbas  23565  ordtrest2lem  23576  ordtrest2  23577  pnfnei  23593  mnfnei  23594  tgcn  23625  cnconst  23657  cnindis  23665  lmss  23671  ordtt1  23752  discmp  23771  1stcrest  23826  2ndcdisj  23830  cldllycmp  23869  txbas  23941  ptpjpre1  23945  ptuni2  23950  ptbasin  23951  ptbasfi  23955  ptopn2  23958  txbasval  23980  ptpjopn  23986  ptclsg  23989  dfac14lem  23991  xkoccn  23993  ptcnp  23996  upxp  23997  ptrescn  24013  txkgen  24026  xkoptsub  24028  xkopt  24029  xkoco1cn  24031  xkoco2cn  24032  xkococn  24034  xkoinjcn  24061  ordthmeolem  24175  ptuncnv  24181  nrmhaus  24200  fbssint  24212  fbfinnfr  24215  fbasrn  24258  isufil2  24282  filufint  24294  rnelfm  24327  fmfnfmlem2  24329  fmfnfmlem3  24330  fmfnfmlem4  24331  fmfnfm  24332  flimtopon  24344  flimclslem  24358  fclstopon  24386  fclscf  24399  flimfnfcls  24402  alexsublem  24418  alexsubALTlem3  24423  alexsubALTlem4  24424  ptcmplem2  24427  tmdgsum2  24470  symgtgp  24480  cldsubg  24485  qustgplem  24495  tgptsmscld  24525  tsmsxplem1  24527  imasdsf1olem  24747  blssps  24798  blss  24799  stdbdxmet  24889  methaus  24894  metrest  24898  nrginvrcn  25066  nmoeq0  25110  blssioo  25169  xrtgioo  25181  xrsxmet  25184  reconnlem1  25201  reconnlem2  25202  xrge0tsms  25209  elcncf1di  25271  iccpnfcnv  25320  evth  25335  lebnumlem1  25337  lebnumlem2  25338  lebnumlem3  25339  nmoleub3  25495  minveclem3b  25804  ivthlem2  25828  ivthlem3  25829  elovolm  25851  ovolmge0  25853  ovoliun  25881  ovolicc2lem3  25895  ovolicc2  25898  voliunlem3  25928  dyaddisj  25972  dyadmax  25974  opnmblALT  25979  ismbfd  26015  ismbf2d  26016  mbfimaopnlem  26031  mbfimaopn2  26033  i1fmullem  26070  i1fres  26081  itg1climres  26090  mbfi1fseqlem4  26094  itg2lcl  26103  itgsplitioo  26213  ellimc2  26252  rolle  26365  dvlip  26368  dvge0  26381  dvne0  26386  lhop1lem  26388  tdeglem4  26433  degltlem1  26445  deg1nn0clb  26463  deg1lt0  26464  dvdsq1p  26536  ply1rem  26539  fta1g  26543  elply2  26569  plyf  26571  ne0p  26580  plyeq0lem  26584  plypf1  26586  0dgrb  26620  coe1termlem  26632  dgrcolem2  26648  plymul0or  26654  plyrem  26681  fta1  26684  rnplynfin  26685  quotcan  26687  rngunsnply  26693  aalioulem3  26718  eff1olem  26933  lognegb  26975  eflogeq  26987  argregt0  26995  argrege0  26996  tanarg  27004  cxpexp  27053  cxpeq0  27063  mulcxp  27070  cxpeq  27142  atans2  27316  scvxcvx  27370  dmgmaddn0  27407  isppw2  27499  vmappw  27500  vmacl  27502  efvmacl  27504  isnsqf  27519  mumullem2  27564  sqff1o  27566  dvdsppwf1o  27570  ppiublem1  27586  vmalelog  27589  chtublem  27595  fsumvma  27597  perfectlem2  27614  perfect  27615  bposlem1  27668  lgsmod  27707  lgsne0  27719  lgsdirnn0  27728  lgsqr  27735  lgsdchr  27739  gausslemma2dlem1a  27749  gausslemma2dlem6  27756  lgseisenlem2  27760  lgsquadlem1  27764  lgsquadlem2  27765  2lgslem1b  27776  2sqlem2  27802  mul2sq  27803  2sqlem7  27808  dchrisum0fno1  27895  pntrsumbnd2  27951  ostthlem1  28011  ostth2lem2  28018  ostth3  28022  ostth  28023  nolesgn2ores  28086  nogesgn1ores  28088  nolt02o  28109  nogt01o  28110  nosupbnd2  28130  noinfbnd2lem1  28144  noetasuplem4  28150  noetainflem4  28154  maxs1  28183  mins2  28186  ltsne  28188  eqcuts3  28247  cuteq1  28260  madef  28279  ltslpss  28351  lrrecfr  28386  addsval  28405  addsproplem2  28413  addsuniflem  28444  addbdaylem  28460  negsid  28484  negsunif  28498  mulsproplem5  28563  mulsproplem6  28564  mulsproplem7  28565  mulsproplem8  28566  mulsproplem9  28567  lemulsd  28581  sltmuls1  28590  sltmuls2  28591  ltmuls2  28614  muls0ord  28628  precsexlem8  28657  precsexlem9  28658  precsexlem11  28660  elons2  28701  oncutlt  28707  bdayons  28719  onaddscl  28720  onmulscl  28721  nnsge1  28786  n0fincut  28798  n0subs  28806  dfnns2  28815  eucliddivs  28819  znegscl  28835  zaddscl  28837  zmulscld  28840  elzn0s  28841  eln0zs  28843  n0seo  28864  zseo  28865  bdaypw2n0bndlem  28906  bdaypw2n0bnd  28907  z12no  28919  z12addscl  28920  z12negscl  28921  z12shalf  28923  z12zsodd  28925  z12sge0  28926  z12bdaylem  28927  bdayfinlem  28929  recut  28937  elreno2  28938  remulscllem1  28943  colinearalg  29545  axpasch  29576  axlowdimlem16  29592  axlowdimlem17  29593  axlowdim  29596  axcontlem2  29600  axcontlem4  29602  axcontlem7  29605  lpvtx  29703  edglnl  29778  numedglnl  29779  usgredgop  29808  usgrexmplef  29897  uhgrspansubgrlem  29928  uhgrspan1  29941  nbusgredgeu0  30006  nb3grprlem2  30019  cusgrsize2inds  30091  vtxd0nedgb  30126  rusgrpropnb  30221  upgrwlkvtxedg  30282  wlkp1lem1  30309  wlkp1lem6  30314  wlkp1lem8  30316  usgr2wlkneq  30399  crctcshwlk  30468  crctcsh  30470  iswwlksnon  30499  wlkiswwlks1  30513  wwlksnextbi  30540  wwlksnextproplem2  30556  wspthsnonn0vne  30563  clwlkclwwlklem2  30648  clwwisshclwws  30663  erclwwlktr  30670  clwwlkel  30694  clwwlkext2edg  30704  erclwwlkntr  30719  clwlknf1oclwwlknlem2  30730  clwlknf1oclwwlknlem3  30731  clwlknf1oclwwlkn  30732  clwwlknonccat  30744  0wlkons1  30769  3wlkdlem6  30823  eupth2eucrct  30875  frgrwopreglem2  30971  2clwwlk2clwwlk  31008  wlkl0  31025  nvmul0or  31309  ipasslem5  31494  ipasslem11  31499  hvmul0or  31684  his6  31758  hhssnv  31923  ocsh  31942  ocin  31955  shsidmi  32043  chnlen0  32103  h1de2bi  32213  h1de2ctlem  32214  h1de2ci  32215  spansni  32216  3oalem1  32321  nmcexi  32685  atcveq0  33007  chcv1  33014  cdjreui  33091  cdj3lem2b  33096  xrge0tsmsd  33733  1fldgenq  33988  rngunsnply1  34249  psrmonmul  34293  ccfldextdgrr  34415  ordtrest2NEWlem  34665  ordtrest2NEW  34666  xrge0iifcnv  34676  esumc  34794  esumpcvgval  34821  ballotlemfc0  35236  ballotlemfcc  35237  axprALT2  35857  fineqvnttrclse  35933  gblacfnacd  36070  vonf1oonfo  36090  onvfowev  36091  subfacp1lem4  36156  subfacp1lem5  36157  erdszelem8  36171  sconnpi1  36212  cvmsss2  36247  cvmlift2lem12  36287  satfv0  36331  satfv0fun  36344  satf00  36347  sat1el2xp  36352  fmla0xp  36356  fmlasucdisj  36372  satffunlem1lem1  36375  satffunlem2lem1  36377  dmopab3rexdif  36378  msubco  36504  msubvrs  36533  ellcsrspsn  36614  sinccvglem  36645  mirimanoffr  36668  untsucf  36690  nnuni  36707  dfrdg2  36772  colineardim1  37041  btwnconn1lem14  37080  segleantisym  37095  colinbtwnle  37098  outsidele  37112  lineunray  37127  linethru  37133  nmulprop  37154  nmuladdss  37177  elicc3  37320  opnregcld  37333  cldregopn  37334  fnejoin2  37372  bj-isrvec  38483  dissneqlem  38531  icorempo  38542  relowlssretop  38554  relowlpssretop  38555  rdgssun  38569  finxpsuclem  38588  ptrecube  38806  poimirlem6  38812  poimirlem7  38813  poimirlem16  38822  poimirlem17  38823  poimirlem19  38825  poimirlem20  38826  poimirlem21  38827  poimirlem22  38828  poimirlem23  38829  poimirlem24  38830  poimirlem25  38831  poimirlem26  38832  poimirlem27  38833  poimirlem29  38835  poimirlem30  38836  poimirlem31  38837  poimirlem32  38838  itg2addnclem3  38859  ftc1anclem6  38884  dvasin  38890  unirep  38916  sdclem2  38942  ssbnd  38988  prdsbnd  38993  cntotbnd  38996  heibor1lem  39009  rrnequiv  39035  ismndo2  39074  grpoeqdivid  39081  isdrngo3  39159  crngohomfo  39206  0idl  39225  1idl  39226  divrngidl  39228  smprngopr  39252  prnc  39267  ispridlc  39270  disjimeceqim  40002  riotaclbgBAD  40277  lshpdisj  40310  lsateln0  40318  lsatcveq0  40355  opnlen0  40511  cmtbr4N  40578  cvrnbtwn2  40598  cvrnbtwn4  40602  atcvreq0  40637  cvlatexch1  40659  exatleN  40727  atlelt  40761  ps-2  40801  llnn0  40839  lplnn0N  40870  islpln2a  40871  lvoln0N  40914  islvol2aN  40915  4at  40936  dalemcea  40983  dalem3  40987  pmapglb2N  41094  pmapglb2xN  41095  cdlema1N  41114  cdlemb  41117  paddasslem17  41159  llnexchb2lem  41191  llnexchb2  41192  lhpat3  41369  ltrnid  41458  trlne  41508  cdlemc4  41517  cdleme11h  41589  cdlemednuN  41623  cdlemg1a  41893  tendoeq2  42097  tendoid0  42148  dva1dim  42308  dib1dim  42488  dihlatat  42660  dochkrshp4  42712  dochkr1  42801  lclkrlem2e  42834  lcfrlem16  42881  lcfrlem28  42893  mapd0  42988  hdmap14lem13  43203  eqresfnbd  43553  expeq1d  43647  expeqidd  43648  dvdsexpnn0  43652  reladdrsub  43702  sn-remul0ord  43725  sn-negex12  43734  sn-mullid  43753  sn-mul02  43782  nn0addcom  43792  nn0mulcom  43796  zmulcomlem  43797  mulgt0con1d  43800  mulgt0con2d  43801  sn-sup2  43821  frlmsnic  43870  evlselvlem  43882  prjspnnorm  43927  elrfi  43971  mrefg2  43984  eldiophb  44034  eldioph2b  44040  diophin  44049  diophun  44050  rexzrexnn0  44077  eldioph4b  44084  diophren  44086  rencldnfilem  44093  pellexlem6  44107  jm2.19  44266  rmydioph  44287  expdiophlem1  44294  expdioph  44296  lnr2i  44383  lpirlnr  44384  hbtlem2  44391  hbtlem4  44393  hbtlem6  44396  dgrsub2  44402  dgraa0p  44416  nlimsuc  44703  dfsucon  44785  radcnvrat  45559  pm14.24  45676  addrcom  45717  modelaxreplem1  46232  ormklocald  48159  afveu  48496  dfafn5b  48504  rlimdmafv  48520  afv2eu  48581  rlimdmafv2  48601  el1fzopredsuc  48669  minusmod5ne  48698  modmknepk  48711  elsetpreimafvssdm  48741  imasetpreimafvbijlemfo  48760  sprvalpw  48835  prprvalpw  48870  reupr  48877  fmtnofac2lem  48926  proththdlem  48971  perfectALTVlem2  49093  perfectALTV  49094  gbowpos  49130  gbowgt5  49133  gboge9  49135  nnsum4primesodd  49167  nnsum4primesoddALTV  49168  uhgrimedgi  49261  isuspgrim0  49265  isuspgrimlem  49266  upgrimpths  49280  clnbgrgrim  49305  grimedg  49306  grtrissvtx  49315  stgredgiun  49329  stgrvtx0  49333  isubgr3stgrlem7  49343  grlimgrtrilem2  49373  gpgiedgdmellem  49417  gpgvtxel2  49419  gpgvtx0  49424  gpgvtx1  49425  gpgusgralem  49427  gpgedgvtx0  49432  gpgedgvtx1  49433  gpgedg2ov  49437  gpgedg2iv  49438  gpgnbgrvtx0  49445  gpgnbgrvtx1  49446  pgnbgreunbgr  49496  ringcinvALTV  49680  lazssaz  49730  adcnlaz  49734  gzilaz  49735  lazmulzcl  49737  lazaddcl  49738  smprngprmrng  49767  lincellss  49869  lindsrng01  49911  suppdm  49953  nnpw2pb  50030  0aryfvalel  50077  0aryfvalelfv  50078  itsclc0xyqsolr  50212  infsubc  50505  infsubc2  50506