Theorem syl5ibrcom 249

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  biimprcd  252  iftrueb  4490  elsn2g  4620  preq1b  4801  elpreqprb  4823  reusv3  5359  alxfr  5361  reuhypd  5373  axpr  5381  opth1  5440  euotd  5479  otiunsndisj  5486  tz7.2  5626  frsn  5731  dmopab2rex  5889  elsnxp  6273  reuop  6275  dfpo2  6278  ordtri1  6374  ordtri3  6377  fvmptdv2  6989  fveqressseq  7055  foco2  7085  fsn  7112  fnsnbg  7143  fnsnbOLD  7145  fmptsng  7147  fmptsnd  7148  fconst2g  7182  fnprb  7187  fntpb  7188  funfvima  7209  soisoi  7307  isores3  7314  eqfunresadj  7339  riotaeqimp  7374  eusvobj2  7383  ovmpodv2  7549  f1opw2  7646  sorpssun  7708  sorpssin  7709  oneqmin  7778  nlimsucg  7817  onzsl  7821  tfinds  7835  funcnvuni  7908  mptcnfimad  7962  opiota  8035  mposn  8076  mpof1o2d  8099  frpoins3xpg  8114  frpoins3xp3g  8115  poxp2  8117  xpord2pred  8119  sexp2  8120  poxp3  8124  xpord3pred  8126  sexp3  8127  xpord3inddlem  8128  suppssov1  8171  suppssov2  8172  suppssfv  8176  brtpos  8209  frrlem12  8272  frrlem13  8273  seqomlem1  8415  seqomlem2  8416  omordi  8529  omord  8531  omwordi  8534  oeeui  8566  nnmordi  8595  nnmord  8596  nnmwordi  8599  nnawordex  8601  nnaordex  8602  nneob  8620  omsmolem  8621  eldifsucnn  8628  qsss  8751  eroveu  8788  mapsncnv  8869  ralxpmap  8872  elixpsn  8913  ixpsnf1o  8914  boxcutc  8917  pw2f1olem  9047  2pwne  9099  mapxpen  9109  mapunen  9112  php  9169  onomeneq  9176  unxpdomlem2  9195  en1eqsnbi  9214  isfiniteg  9238  fofinf1o  9269  f1opwfi  9293  elfiun  9370  oieu  9481  brwdom2  9515  wdomtr  9517  ixpiunwdom  9532  en3lplem1  9561  suc11reg  9568  inf3lemd  9576  cantnfvalf  9614  cantnflt  9621  cantnfp1lem3  9629  cantnflem2  9639  ttrcltr  9665  rnttrcl  9671  ttrclselem1  9674  r1tr  9728  updjud  9886  dfac8alem  9979  wdomnumr  10014  isinfcard  10042  aceq3lem  10070  dfac5lem4  10076  dfac5lem4OLD  10078  dfac5  10079  dfac2b  10081  coftr  10224  fin23lem28  10291  fin23lem29  10292  fin1a2lem11  10361  fin1a2lem12  10362  fin1a2lem13  10363  hsmexlem9  10376  axdclem  10470  pwcfsdom  10535  gchdomtri  10581  fpwwe2  10595  gchpwdom  10622  gchhar  10631  addnidpi  10853  nqereu  10881  genpv  10951  genpdm  10954  distrlem5pr  10979  mulrid  11173  ltne  11274  mul02  11355  cnegex  11358  mul0or  11821  negfi  12135  sup2  12142  supaddc  12153  supadd  12154  supmul1  12155  supmul  12158  creur  12183  creui  12184  cju  12185  nnsub  12251  un0addcl  12508  un0mulcl  12509  nn0sub  12525  elz2  12580  zaddcl  12605  suprzcl2  12933  qmulz  12946  qre  12948  qnegcl  12961  elpqb  12971  xrmax1  13172  xrmin2  13175  max1ALT  13183  xlesubadd  13260  xmulass  13284  xlemul1a  13285  xrsupexmnf  13302  xrinfmexpnf  13303  xrub  13309  iccid  13388  fzsn  13565  fzsuc2  13581  fz1sbc  13599  elfzp12  13602  modmuladd  13920  seqid3  14053  bcval5  14325  bcpasc  14328  hashbnd  14343  hashnnn0genn0  14350  hashprg  14402  hashfzo  14436  tpfo  14507  wrdl1s1  14622  ccats1alpha  14627  cats1un  14728  s7f1o  14973  shftlem  15075  replim  15134  absmod0  15321  absz  15329  rlimdm  15569  summolem2  15734  summo  15735  zsum  15736  fsum  15738  fsummulc2  15802  fsumconst  15808  fsum00  15817  incexclem  15857  isumsplit  15861  infcvgaux1i  15878  prodmolem2  15956  prodmo  15957  zprod  15958  fprod  15962  prodsn  15983  prodsnf  15985  fprodconst  15999  ruclem2  16255  fzo0dvdseq  16348  bitsf1ocnv  16469  sadcaddlem  16482  smueqlem  16515  gcdabs1  16554  bezoutlem1  16564  bezoutlem3  16566  bezoutlem4  16567  dvdsgcd  16569  dvdsmulgcd  16581  lcmgcdeq  16637  lcmf  16658  lcmfunsnlem1  16662  lcmfunsnlem2lem2  16664  isprm2lem  16706  dvdsprime  16712  isprm5  16733  coprm  16737  prmdvdsexpr  16743  rpexp  16748  phibndlem  16796  dfphi2  16800  hashgcdlem  16814  odzdvds  16822  nnoddn2prm  16838  pythagtriplem1  16843  iserodd  16862  pceulem  16872  pcqmul  16880  pcqcl  16883  pcxnn0cl  16887  pcxcl  16888  pcneg  16901  pcabs  16902  pcgcd1  16904  pcz  16908  pcprmpw2  16909  pcprmpw  16910  dvdsprmpweqle  16913  difsqpwdvds  16914  pcaddlem  16915  pcadd  16916  pcmpt  16919  pockthg  16933  prmreclem5  16947  4sqlem4  16979  mul4sq  16981  vdwapun  17001  vdwlem2  17009  vdwlem6  17013  vdwlem8  17015  vdwlem13  17020  0ram  17047  ram0  17049  ramcl  17056  cshwsiun  17126  wunress  17276  firest  17452  isssc  17844  pospo  18366  latnlej  18479  gsumval2a  18710  xpsmnd0  18803  mnd1id  18805  0subm  18842  mulgnn0p1  19118  mulgnn0ass  19143  cyccom  19235  gicsubgen  19310  symg1bas  19422  snsymgefmndeq  19426  psgnunilem1  19524  psgnunilem2  19526  mndodcongi  19574  oddvdsnn0  19575  odnncl  19576  oddvds  19578  odeq  19581  odeq1  19591  pgpfi2  19637  sylow2a  19650  sylow2blem3  19653  sylow3lem6  19663  lsmelvalm  19682  lsmsubm  19684  lsmsubg  19685  lsmmod  19706  lsmdisj2  19713  efgmnvl  19745  efgtlen  19757  efgs1b  19767  efgrelexlemb  19781  efgredeu  19783  efgcpbllemb  19786  frgpuptinv  19802  frgpup3lem  19808  qusabl  19896  frgpnabllem1  19904  cyggeninv  19914  cyggenod  19915  gsumval3eu  19935  dprdssv  20049  dprdfeq0  20055  dprdsubg  20057  dprddisj2  20072  ablfacrp  20099  pgpfac1lem3  20110  pgpfaclem2  20115  xpsring1d  20369  dvreq1  20447  irredn1  20462  nzrunit  20561  ringcinv  20708  rrgeq0  20737  domneq0  20745  drngmul0orOLD  20798  isabvd  20849  abvdom  20867  issrngd  20892  lmodfopnelem2  20954  lss1d  21018  lspsneq0  21067  lbspss  21137  lsmcl  21138  lvecvs0or  21166  lspindpi  21190  lidl1el  21284  lpiss  21387  lidldvgen  21392  qsssubdrg  21466  zringlpirlem1  21502  pzriprnglem6  21526  pzriprnglem12  21532  znfld  21600  znunit  21603  znrrg  21605  cygznlem3  21609  frgpcyg  21613  psgnghm  21620  ipeq0  21678  cssincl  21728  lsmcss  21732  obselocv  21768  dsmmacl  21781  dsmmlss  21784  mplsubrglem  22043  mplmonmul  22077  mplcoe5lem  22080  mhpsclcl  22200  mhpvarcl  22201  psdmul  22219  coe1tmmul2  22327  coe1tmmul  22328  pf1ind  22406  mat1dimelbas  22519  mdetralt  22656  mdetunilem2  22661  mdetunilem7  22666  mdetunilem9  22668  maducoeval2  22688  chpscmat  22890  chfacfscmulgsum  22908  chfacfpmmulgsum  22912  istopon  22960  eltg3  23010  tgidm  23028  clsval2  23098  opncldf1  23132  restbas  23206  tgrest  23207  restcld  23220  restcldr  23222  restcls  23229  restntr  23230  ordtbas2  23239  ordtbas  23240  ordtrest2lem  23251  ordtrest2  23252  pnfnei  23268  mnfnei  23269  tgcn  23300  cnconst  23332  cnindis  23340  lmss  23346  ordtt1  23427  discmp  23446  1stcrest  23501  2ndcdisj  23504  cldllycmp  23543  txbas  23615  ptpjpre1  23619  ptuni2  23624  ptbasin  23625  ptbasfi  23629  ptopn2  23632  txbasval  23654  ptpjopn  23660  ptclsg  23663  dfac14lem  23665  xkoccn  23667  ptcnp  23670  upxp  23671  ptrescn  23687  txkgen  23700  xkoptsub  23702  xkopt  23703  xkoco1cn  23705  xkoco2cn  23706  xkococn  23708  xkoinjcn  23735  ordthmeolem  23849  ptuncnv  23855  nrmhaus  23874  fbssint  23886  fbfinnfr  23889  fbasrn  23932  isufil2  23956  filufint  23968  rnelfm  24001  fmfnfmlem2  24003  fmfnfmlem3  24004  fmfnfmlem4  24005  fmfnfm  24006  flimtopon  24018  flimclslem  24032  fclstopon  24060  fclscf  24073  flimfnfcls  24076  alexsublem  24092  alexsubALTlem3  24097  alexsubALTlem4  24098  ptcmplem2  24101  tmdgsum2  24144  symgtgp  24154  cldsubg  24159  qustgplem  24169  tgptsmscld  24199  tsmsxplem1  24201  imasdsf1olem  24421  blssps  24472  blss  24473  stdbdxmet  24563  methaus  24568  metrest  24572  nrginvrcn  24740  nmoeq0  24784  blssioo  24843  xrtgioo  24855  xrsxmet  24858  reconnlem1  24875  reconnlem2  24876  xrge0tsms  24883  elcncf1di  24945  iccpnfcnv  24994  evth  25009  lebnumlem1  25011  lebnumlem2  25012  lebnumlem3  25013  nmoleub3  25169  minveclem3b  25478  ivthlem2  25502  ivthlem3  25503  elovolm  25525  ovolmge0  25527  ovoliun  25555  ovolicc2lem3  25569  ovolicc2  25572  voliunlem3  25602  dyaddisj  25646  dyadmax  25648  opnmblALT  25653  ismbfd  25689  ismbf2d  25690  mbfimaopnlem  25705  mbfimaopn2  25707  i1fmullem  25744  i1fres  25755  itg1climres  25764  mbfi1fseqlem4  25768  itg2lcl  25777  itgsplitioo  25888  ellimc2  25927  rolle  26040  dvlip  26043  dvge0  26056  dvne0  26061  lhop1lem  26063  tdeglem4  26108  degltlem1  26120  deg1nn0clb  26138  deg1lt0  26139  dvdsq1p  26211  ply1rem  26214  fta1g  26218  elply2  26244  plyf  26246  ne0p  26255  plyeq0lem  26258  plypf1  26260  0dgrb  26294  coe1termlem  26306  dgrcolem2  26322  plymul0or  26330  plyrem  26357  fta1  26360  quotcan  26361  aalioulem3  26386  eff1olem  26601  lognegb  26643  eflogeq  26655  argregt0  26663  argrege0  26664  tanarg  26672  cxpexp  26721  cxpeq0  26731  mulcxp  26738  cxpeq  26810  atans2  26984  scvxcvx  27038  dmgmaddn0  27075  isppw2  27167  vmappw  27168  vmacl  27170  efvmacl  27172  isnsqf  27187  mumullem2  27232  sqff1o  27234  dvdsppwf1o  27238  ppiublem1  27254  vmalelog  27257  chtublem  27263  fsumvma  27265  perfectlem2  27282  perfect  27283  bposlem1  27336  lgsmod  27375  lgsne0  27387  lgsdirnn0  27396  lgsqr  27403  lgsdchr  27407  gausslemma2dlem1a  27417  gausslemma2dlem6  27424  lgseisenlem2  27428  lgsquadlem1  27432  lgsquadlem2  27433  2lgslem1b  27444  2sqlem2  27470  mul2sq  27471  2sqlem7  27476  dchrisum0fno1  27563  pntrsumbnd2  27619  ostthlem1  27679  ostth2lem2  27686  ostth3  27690  ostth  27691  nolesgn2ores  27724  nogesgn1ores  27726  nolt02o  27747  nogt01o  27748  nosupbnd2  27768  noinfbnd2lem1  27782  noetasuplem4  27788  noetainflem4  27792  maxs1  27821  mins2  27824  ltsne  27826  eqcuts3  27885  cuteq1  27898  madef  27917  ltslpss  27989  lrrecfr  28024  addsval  28043  addsproplem2  28051  addsuniflem  28082  addbdaylem  28098  negsid  28122  negsunif  28136  mulsproplem5  28201  mulsproplem6  28202  mulsproplem7  28203  mulsproplem8  28204  mulsproplem9  28205  lemulsd  28219  sltmuls1  28228  sltmuls2  28229  ltmuls2  28252  muls0ord  28266  precsexlem8  28295  precsexlem9  28296  precsexlem11  28298  elons2  28339  oncutlt  28345  bdayons  28357  onaddscl  28358  onmulscl  28359  nnsge1  28424  n0fincut  28436  n0subs  28444  dfnns2  28453  eucliddivs  28457  znegscl  28473  zaddscl  28475  zmulscld  28478  elzn0s  28479  eln0zs  28481  n0seo  28502  zseo  28503  bdaypw2n0bndlem  28544  bdaypw2n0bnd  28545  z12no  28557  z12addscl  28558  z12negscl  28559  z12shalf  28561  z12zsodd  28563  z12sge0  28564  z12bdaylem  28565  bdayfinlem  28567  recut  28575  elreno2  28576  remulscllem1  28581  colinearalg  29068  axpasch  29099  axlowdimlem16  29115  axlowdimlem17  29116  axlowdim  29119  axcontlem2  29123  axcontlem4  29125  axcontlem7  29128  lpvtx  29226  edglnl  29301  numedglnl  29302  usgredgop  29328  usgrexmplef  29417  uhgrspansubgrlem  29448  uhgrspan1  29461  nbusgredgeu0  29526  nb3grprlem2  29539  cusgrsize2inds  29611  vtxd0nedgb  29646  rusgrpropnb  29741  upgrwlkvtxedg  29802  wlkp1lem1  29829  wlkp1lem6  29834  wlkp1lem8  29836  usgr2wlkneq  29913  crctcshwlk  29979  crctcsh  29981  iswwlksnon  30010  wlkiswwlks1  30024  wwlksnextbi  30051  wwlksnextproplem2  30067  wspthsnonn0vne  30074  clwlkclwwlklem2  30159  clwwisshclwws  30174  erclwwlktr  30181  clwwlkel  30205  clwwlkext2edg  30215  erclwwlkntr  30230  clwlknf1oclwwlknlem2  30241  clwlknf1oclwwlknlem3  30242  clwlknf1oclwwlkn  30243  clwwlknonccat  30255  0wlkons1  30280  3wlkdlem6  30324  eupth2eucrct  30376  frgrwopreglem2  30472  2clwwlk2clwwlk  30509  wlkl0  30526  nvmul0or  30810  ipasslem5  30995  ipasslem11  31000  hvmul0or  31185  his6  31259  hhssnv  31424  ocsh  31443  ocin  31456  shsidmi  31544  chnlen0  31604  h1de2bi  31714  h1de2ctlem  31715  h1de2ci  31716  spansni  31717  3oalem1  31822  nmcexi  32186  atcveq0  32508  chcv1  32515  cdjreui  32592  cdj3lem2b  32597  xrge0tsmsd  33214  1fldgenq  33470  psrmonmul  33808  ccfldextdgrr  33930  ordtrest2NEWlem  34180  ordtrest2NEW  34181  xrge0iifcnv  34191  esumc  34309  esumpcvgval  34336  ballotlemfc0  34751  ballotlemfcc  34752  fissorduni  35346  axprALT2  35366  fineqvnttrclse  35381  gblacfnacd  35406  vonf1oonfo  35419  onvfowev  35420  subfacp1lem4  35494  subfacp1lem5  35495  erdszelem8  35509  sconnpi1  35550  cvmsss2  35585  cvmlift2lem12  35625  satfv0  35669  satfv0fun  35682  satf00  35685  sat1el2xp  35690  fmla0xp  35694  fmlasucdisj  35710  satffunlem1lem1  35713  satffunlem2lem1  35715  dmopab3rexdif  35716  msubco  35842  msubvrs  35871  ellcsrspsn  35952  sinccvglem  35983  untsucf  36021  nnuni  36038  dfrdg2  36104  colineardim1  36372  btwnconn1lem14  36411  segleantisym  36426  colinbtwnle  36429  outsidele  36443  lineunray  36458  linethru  36464  nmulprop  36501  elicc3  36638  opnregcld  36651  cldregopn  36652  fnejoin2  36690  bj-isrvec  37747  dissneqlem  37795  icorempo  37806  relowlssretop  37818  relowlpssretop  37819  rdgssun  37833  finxpsuclem  37852  lindsenlbs  38075  ptrecube  38080  poimirlem6  38086  poimirlem7  38087  poimirlem16  38096  poimirlem17  38097  poimirlem19  38099  poimirlem20  38100  poimirlem21  38101  poimirlem22  38102  poimirlem23  38103  poimirlem24  38104  poimirlem25  38105  poimirlem26  38106  poimirlem27  38107  poimirlem29  38109  poimirlem30  38110  poimirlem31  38111  poimirlem32  38112  itg2addnclem3  38133  ftc1anclem6  38158  dvasin  38164  unirep  38174  sdclem2  38202  ssbnd  38248  prdsbnd  38253  cntotbnd  38256  heibor1lem  38269  rrnequiv  38295  ismndo2  38334  grpoeqdivid  38341  isdrngo3  38419  crngohomfo  38466  0idl  38485  1idl  38486  divrngidl  38488  smprngopr  38512  prnc  38527  ispridlc  38530  disjimeceqim  39264  riotaclbgBAD  39539  lshpdisj  39572  lsateln0  39580  lsatcveq0  39617  opnlen0  39773  cmtbr4N  39840  cvrnbtwn2  39860  cvrnbtwn4  39864  atcvreq0  39899  cvlatexch1  39921  exatleN  39989  atlelt  40023  ps-2  40063  llnn0  40101  lplnn0N  40132  islpln2a  40133  lvoln0N  40176  islvol2aN  40177  4at  40198  dalemcea  40245  dalem3  40249  pmapglb2N  40356  pmapglb2xN  40357  cdlema1N  40376  cdlemb  40379  paddasslem17  40421  llnexchb2lem  40453  llnexchb2  40454  lhpat3  40631  ltrnid  40720  trlne  40770  cdlemc4  40779  cdleme11h  40851  cdlemednuN  40885  cdlemg1a  41155  tendoeq2  41359  tendoid0  41410  dva1dim  41570  dib1dim  41750  dihlatat  41922  dochkrshp4  41974  dochkr1  42063  lclkrlem2e  42096  lcfrlem16  42143  lcfrlem28  42155  mapd0  42250  hdmap14lem13  42465  eqresfnbd  42812  expeq1d  42894  expeqidd  42895  dvdsexpnn0  42904  reladdrsub  42955  sn-remul0ord  42978  sn-negex12  42987  sn-mullid  43006  sn-mul02  43035  nn0addcom  43045  nn0mulcom  43049  zmulcomlem  43050  mulgt0con1d  43053  mulgt0con2d  43054  sn-sup2  43074  frlmsnic  43119  evlselvlem  43131  prjspner1  43169  elrfi  43236  mrefg2  43249  eldiophb  43299  eldioph2b  43305  diophin  43314  diophun  43315  rexzrexnn0  43342  eldioph4b  43349  diophren  43351  rencldnfilem  43358  pellexlem6  43372  jm2.19  43531  rmydioph  43552  expdiophlem1  43559  expdioph  43561  lnr2i  43654  lpirlnr  43655  hbtlem2  43662  hbtlem4  43664  hbtlem6  43667  dgrsub2  43673  dgraa0p  43687  rngunsnply  43707  nlimsuc  43978  dfsucon  44060  radcnvrat  44851  pm14.24  44969  addrcom  45011  modelaxreplem1  45515  ormklocald  47411  natlocalincr  47413  afveu  47708  dfafn5b  47716  rlimdmafv  47732  afv2eu  47793  rlimdmafv2  47813  el1fzopredsuc  47881  minusmod5ne  47910  modmknepk  47923  elsetpreimafvssdm  47953  imasetpreimafvbijlemfo  47972  sprvalpw  48047  prprvalpw  48082  reupr  48089  fmtnofac2lem  48138  proththdlem  48183  perfectALTVlem2  48305  perfectALTV  48306  gbowpos  48342  gbowgt5  48345  gboge9  48347  nnsum4primesodd  48379  nnsum4primesoddALTV  48380  uhgrimedgi  48473  isuspgrim0  48477  isuspgrimlem  48478  upgrimpths  48492  clnbgrgrim  48517  grimedg  48518  grtrissvtx  48527  stgredgiun  48541  stgrvtx0  48545  isubgr3stgrlem7  48555  grlimgrtrilem2  48585  gpgiedgdmellem  48629  gpgvtxel2  48631  gpgvtx0  48636  gpgvtx1  48637  gpgusgralem  48639  gpgedgvtx0  48644  gpgedgvtx1  48645  gpgedg2ov  48649  gpgedg2iv  48650  gpgnbgrvtx0  48657  gpgnbgrvtx1  48658  pgnbgreunbgr  48708  ringcinvALTV  48893  lincellss  49009  lindsrng01  49051  suppdm  49093  nnpw2pb  49170  0aryfvalel  49217  0aryfvalelfv  49218  itsclc0xyqsolr  49352  infsubc  49642  infsubc2  49643