Theorem syl5ibrcom 247

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  biimprcd  250  iftrueb  4504  elsn2g  4631  preq1b  4813  elpreqprb  4835  reusv3  5363  alxfr  5365  reuhypd  5377  axpr  5385  opth1  5438  euotd  5476  otiunsndisj  5483  tz7.2  5624  frsn  5729  dmopab2rex  5884  elsnxp  6267  reuop  6269  dfpo2  6272  ordtri1  6368  ordtri3  6371  fvmptdv2  6989  fveqressseq  7054  foco2  7084  fsn  7110  fnsnbg  7141  fnsnbOLD  7143  fmptsng  7145  fmptsnd  7146  fconst2g  7180  fnprb  7185  fntpb  7186  funfvima  7207  soisoi  7306  isores3  7313  eqfunresadj  7338  riotaeqimp  7373  eusvobj2  7382  ovmpodv2  7550  f1opw2  7647  sorpssun  7709  sorpssin  7710  oneqmin  7779  nlimsucg  7821  onzsl  7825  tfinds  7839  funcnvuni  7911  mptcnfimad  7968  opiota  8041  mposn  8085  frpoins3xpg  8122  frpoins3xp3g  8123  poxp2  8125  xpord2pred  8127  sexp2  8128  poxp3  8132  xpord3pred  8134  sexp3  8135  xpord3inddlem  8136  suppssov1  8179  suppssov2  8180  suppssfv  8184  brtpos  8217  frrlem12  8279  frrlem13  8280  seqomlem1  8421  seqomlem2  8422  omordi  8533  omord  8535  omwordi  8538  oeeui  8569  nnmordi  8598  nnmord  8599  nnmwordi  8602  nnawordex  8604  nnaordex  8605  nneob  8623  omsmolem  8624  eldifsucnn  8631  qsss  8752  eroveu  8788  mapsncnv  8869  ralxpmap  8872  elixpsn  8913  ixpsnf1o  8914  boxcutc  8917  pw2f1olem  9050  2pwne  9103  mapxpen  9113  mapunen  9116  php  9177  onomeneq  9184  unxpdomlem2  9205  en1eqsnbi  9228  isfiniteg  9255  fofinf1o  9290  f1opwfi  9314  elfiun  9388  oieu  9499  brwdom2  9533  wdomtr  9535  ixpiunwdom  9550  en3lplem1  9572  suc11reg  9579  inf3lemd  9587  cantnfvalf  9625  cantnflt  9632  cantnfp1lem3  9640  cantnflem2  9650  ttrcltr  9676  rnttrcl  9682  ttrclselem1  9685  r1tr  9736  updjud  9894  dfac8alem  9989  wdomnumr  10024  isinfcard  10052  aceq3lem  10080  dfac5lem4  10086  dfac5lem4OLD  10088  dfac5  10089  dfac2b  10091  coftr  10233  fin23lem28  10300  fin23lem29  10301  fin1a2lem11  10370  fin1a2lem12  10371  fin1a2lem13  10372  hsmexlem9  10385  axdclem  10479  pwcfsdom  10543  gchdomtri  10589  fpwwe2  10603  gchpwdom  10630  gchhar  10639  addnidpi  10861  nqereu  10889  genpv  10959  genpdm  10962  distrlem5pr  10987  mulrid  11179  ltne  11278  mul02  11359  cnegex  11362  mul0or  11825  negfi  12139  sup2  12146  supaddc  12157  supadd  12158  supmul1  12159  supmul  12162  creur  12187  creui  12188  cju  12189  nnsub  12237  un0addcl  12482  un0mulcl  12483  nn0sub  12499  elz2  12554  zaddcl  12580  suprzcl2  12904  qmulz  12917  qre  12919  qnegcl  12932  elpqb  12942  xrmax1  13142  xrmin2  13145  max1ALT  13153  xlesubadd  13230  xmulass  13254  xlemul1a  13255  xrsupexmnf  13272  xrinfmexpnf  13273  xrub  13279  iccid  13358  fzsn  13534  fzsuc2  13550  fz1sbc  13568  elfzp12  13571  modmuladd  13885  seqid3  14018  bcval5  14290  bcpasc  14293  hashbnd  14308  hashnnn0genn0  14315  hashprg  14367  hashfzo  14401  tpfo  14472  wrdl1s1  14586  ccats1alpha  14591  cats1un  14693  s7f1o  14939  shftlem  15041  replim  15089  absmod0  15276  absz  15284  rlimdm  15524  summolem2  15689  summo  15690  zsum  15691  fsum  15693  fsummulc2  15757  fsumconst  15763  fsum00  15771  incexclem  15809  isumsplit  15813  infcvgaux1i  15830  prodmolem2  15908  prodmo  15909  zprod  15910  fprod  15914  prodsn  15935  prodsnf  15937  fprodconst  15951  ruclem2  16207  fzo0dvdseq  16300  bitsf1ocnv  16421  sadcaddlem  16434  smueqlem  16467  gcdabs1  16506  bezoutlem1  16516  bezoutlem3  16518  bezoutlem4  16519  dvdsgcd  16521  dvdsmulgcd  16533  lcmgcdeq  16589  lcmf  16610  lcmfunsnlem1  16614  lcmfunsnlem2lem2  16616  isprm2lem  16658  dvdsprime  16664  isprm5  16684  coprm  16688  prmdvdsexpr  16694  rpexp  16699  phibndlem  16747  dfphi2  16751  hashgcdlem  16765  odzdvds  16773  nnoddn2prm  16789  pythagtriplem1  16794  iserodd  16813  pceulem  16823  pcqmul  16831  pcqcl  16834  pcxnn0cl  16838  pcxcl  16839  pcneg  16852  pcabs  16853  pcgcd1  16855  pcz  16859  pcprmpw2  16860  pcprmpw  16861  dvdsprmpweqle  16864  difsqpwdvds  16865  pcaddlem  16866  pcadd  16867  pcmpt  16870  pockthg  16884  prmreclem5  16898  4sqlem4  16930  mul4sq  16932  vdwapun  16952  vdwlem2  16960  vdwlem6  16964  vdwlem8  16966  vdwlem13  16971  0ram  16998  ram0  17000  ramcl  17007  cshwsiun  17077  wunress  17226  firest  17402  isssc  17789  pospo  18311  latnlej  18422  gsumval2a  18619  xpsmnd0  18712  mnd1id  18714  0subm  18751  mulgnn0p1  19024  mulgnn0ass  19049  cyccom  19142  gicsubgen  19218  symg1bas  19328  snsymgefmndeq  19332  psgnunilem1  19430  psgnunilem2  19432  mndodcongi  19480  oddvdsnn0  19481  odnncl  19482  oddvds  19484  odeq  19487  odeq1  19497  pgpfi2  19543  sylow2a  19556  sylow2blem3  19559  sylow3lem6  19569  lsmelvalm  19588  lsmsubm  19590  lsmsubg  19591  lsmmod  19612  lsmdisj2  19619  efgmnvl  19651  efgtlen  19663  efgs1b  19673  efgrelexlemb  19687  efgredeu  19689  efgcpbllemb  19692  frgpuptinv  19708  frgpup3lem  19714  qusabl  19802  frgpnabllem1  19810  cyggeninv  19820  cyggenod  19821  gsumval3eu  19841  dprdssv  19955  dprdfeq0  19961  dprdsubg  19963  dprddisj2  19978  ablfacrp  20005  pgpfac1lem3  20016  pgpfaclem2  20021  xpsring1d  20249  dvreq1  20327  irredn1  20342  nzrunit  20440  ringcinv  20587  rrgeq0  20616  domneq0  20624  drngmul0orOLD  20677  isabvd  20728  abvdom  20746  issrngd  20771  lmodfopnelem2  20812  lss1d  20876  lspsneq0  20925  lbspss  20996  lsmcl  20997  lvecvs0or  21025  lspindpi  21049  lidl1el  21143  lpiss  21246  lidldvgen  21251  qsssubdrg  21350  zringlpirlem1  21379  pzriprnglem6  21403  pzriprnglem12  21409  znfld  21477  znunit  21480  znrrg  21482  cygznlem3  21486  frgpcyg  21490  psgnghm  21496  ipeq0  21554  cssincl  21604  lsmcss  21608  obselocv  21644  dsmmacl  21657  dsmmlss  21660  mplsubrglem  21920  mplmonmul  21950  mplcoe5lem  21953  mhpsclcl  22041  mhpvarcl  22042  psdmul  22060  coe1tmmul2  22169  coe1tmmul  22170  pf1ind  22249  mat1dimelbas  22365  mdetralt  22502  mdetunilem2  22507  mdetunilem7  22512  mdetunilem9  22514  maducoeval2  22534  chpscmat  22736  chfacfscmulgsum  22754  chfacfpmmulgsum  22758  istopon  22806  eltg3  22856  tgidm  22874  clsval2  22944  opncldf1  22978  restbas  23052  tgrest  23053  restcld  23066  restcldr  23068  restcls  23075  restntr  23076  ordtbas2  23085  ordtbas  23086  ordtrest2lem  23097  ordtrest2  23098  pnfnei  23114  mnfnei  23115  tgcn  23146  cnconst  23178  cnindis  23186  lmss  23192  ordtt1  23273  discmp  23292  1stcrest  23347  2ndcdisj  23350  cldllycmp  23389  txbas  23461  ptpjpre1  23465  ptuni2  23470  ptbasin  23471  ptbasfi  23475  ptopn2  23478  txbasval  23500  ptpjopn  23506  ptclsg  23509  dfac14lem  23511  xkoccn  23513  ptcnp  23516  upxp  23517  ptrescn  23533  txkgen  23546  xkoptsub  23548  xkopt  23549  xkoco1cn  23551  xkoco2cn  23552  xkococn  23554  xkoinjcn  23581  ordthmeolem  23695  ptuncnv  23701  nrmhaus  23720  fbssint  23732  fbfinnfr  23735  fbasrn  23778  isufil2  23802  filufint  23814  rnelfm  23847  fmfnfmlem2  23849  fmfnfmlem3  23850  fmfnfmlem4  23851  fmfnfm  23852  flimtopon  23864  flimclslem  23878  fclstopon  23906  fclscf  23919  flimfnfcls  23922  alexsublem  23938  alexsubALTlem3  23943  alexsubALTlem4  23944  ptcmplem2  23947  tmdgsum2  23990  symgtgp  24000  cldsubg  24005  qustgplem  24015  tgptsmscld  24045  tsmsxplem1  24047  imasdsf1olem  24268  blssps  24319  blss  24320  stdbdxmet  24410  methaus  24415  metrest  24419  nrginvrcn  24587  nmoeq0  24631  blssioo  24690  xrtgioo  24702  xrsxmet  24705  reconnlem1  24722  reconnlem2  24723  xrge0tsms  24730  elcncf1di  24795  iccpnfcnv  24849  evth  24865  lebnumlem1  24867  lebnumlem2  24868  lebnumlem3  24869  nmoleub3  25026  minveclem3b  25335  ivthlem2  25360  ivthlem3  25361  elovolm  25383  ovolmge0  25385  ovoliun  25413  ovolicc2lem3  25427  ovolicc2  25430  voliunlem3  25460  dyaddisj  25504  dyadmax  25506  opnmblALT  25511  ismbfd  25547  ismbf2d  25548  mbfimaopnlem  25563  mbfimaopn2  25565  i1fmullem  25602  i1fres  25613  itg1climres  25622  mbfi1fseqlem4  25626  itg2lcl  25635  itgsplitioo  25746  ellimc2  25785  rolle  25901  dvlip  25905  dvge0  25918  dvne0  25923  lhop1lem  25925  tdeglem4  25972  degltlem1  25984  deg1nn0clb  26002  deg1lt0  26003  dvdsq1p  26075  ply1rem  26078  fta1g  26082  elply2  26108  plyf  26110  ne0p  26119  plyeq0lem  26122  plypf1  26124  0dgrb  26158  coe1termlem  26170  dgrcolem2  26187  plymul0or  26195  plyrem  26220  fta1  26223  quotcan  26224  aalioulem3  26249  eff1olem  26464  lognegb  26506  eflogeq  26518  argregt0  26526  argrege0  26527  tanarg  26535  cxpexp  26584  cxpeq0  26594  mulcxp  26601  cxpeq  26674  atans2  26848  scvxcvx  26903  dmgmaddn0  26940  isppw2  27032  vmappw  27033  vmacl  27035  efvmacl  27037  isnsqf  27052  mumullem2  27097  sqff1o  27099  dvdsppwf1o  27103  ppiublem1  27120  vmalelog  27123  chtublem  27129  fsumvma  27131  perfectlem2  27148  perfect  27149  bposlem1  27202  lgsmod  27241  lgsne0  27253  lgsdirnn0  27262  lgsqr  27269  lgsdchr  27273  gausslemma2dlem1a  27283  gausslemma2dlem6  27290  lgseisenlem2  27294  lgsquadlem1  27298  lgsquadlem2  27299  2lgslem1b  27310  2sqlem2  27336  mul2sq  27337  2sqlem7  27342  dchrisum0fno1  27429  pntrsumbnd2  27485  ostthlem1  27545  ostth2lem2  27552  ostth3  27556  ostth  27557  nolesgn2ores  27591  nogesgn1ores  27593  nolt02o  27614  nogt01o  27615  nosupbnd2  27635  noinfbnd2lem1  27649  noetasuplem4  27655  noetainflem4  27659  maxs1  27684  mins2  27687  sltne  27689  ssltsn  27711  cuteq1  27753  madef  27771  sltlpss  27826  lrrecfr  27857  addsval  27876  addsproplem2  27884  addsuniflem  27915  addsbdaylem  27930  negsid  27954  negsunif  27968  mulsproplem5  28030  mulsproplem6  28031  mulsproplem7  28032  mulsproplem8  28033  mulsproplem9  28034  slemuld  28048  ssltmul1  28057  ssltmul2  28058  sltmul2  28081  muls0ord  28095  precsexlem8  28123  precsexlem9  28124  precsexlem11  28126  elons2  28166  onscutlt  28172  bdayon  28180  onaddscl  28181  onmulscl  28182  nnsge1  28242  n0sfincut  28253  n0subs  28260  dfnns2  28268  eucliddivs  28272  znegscl  28287  zaddscl  28289  zmulscld  28292  elzn0s  28293  eln0zs  28295  n0seo  28314  zseo  28315  zs12negscl  28347  zs12ge0  28349  zs12bday  28350  recut  28354  0reno  28355  remulscllem1  28358  colinearalg  28844  axpasch  28875  axlowdimlem16  28891  axlowdimlem17  28892  axlowdim  28895  axcontlem2  28899  axcontlem4  28901  axcontlem7  28904  lpvtx  29002  edglnl  29077  numedglnl  29078  usgredgop  29104  usgrexmplef  29193  uhgrspansubgrlem  29224  uhgrspan1  29237  nbusgredgeu0  29302  nb3grprlem2  29315  cusgrsize2inds  29388  vtxd0nedgb  29423  rusgrpropnb  29518  upgrwlkvtxedg  29580  wlkp1lem1  29608  wlkp1lem6  29613  wlkp1lem8  29615  usgr2wlkneq  29693  crctcshwlk  29759  crctcsh  29761  iswwlksnon  29790  wlkiswwlks1  29804  wwlksnextbi  29831  wwlksnextproplem2  29847  wspthsnonn0vne  29854  clwlkclwwlklem2  29936  clwwisshclwws  29951  erclwwlktr  29958  clwwlkel  29982  clwwlkext2edg  29992  erclwwlkntr  30007  clwlknf1oclwwlknlem2  30018  clwlknf1oclwwlknlem3  30019  clwlknf1oclwwlkn  30020  clwwlknonccat  30032  0wlkons1  30057  3wlkdlem6  30101  eupth2eucrct  30153  frgrwopreglem2  30249  2clwwlk2clwwlk  30286  wlkl0  30303  nvmul0or  30586  ipasslem5  30771  ipasslem11  30776  hvmul0or  30961  his6  31035  hhssnv  31200  ocsh  31219  ocin  31232  shsidmi  31320  chnlen0  31380  h1de2bi  31490  h1de2ctlem  31491  h1de2ci  31492  spansni  31493  3oalem1  31598  nmcexi  31962  atcveq0  32284  chcv1  32291  cdjreui  32368  cdj3lem2b  32373  xrge0tsmsd  33009  1fldgenq  33279  ccfldextdgrr  33674  ordtrest2NEWlem  33919  ordtrest2NEW  33920  xrge0iifcnv  33930  esumc  34048  esumpcvgval  34075  ballotlemfc0  34491  ballotlemfcc  34492  gblacfnacd  35096  subfacp1lem4  35177  subfacp1lem5  35178  erdszelem8  35192  sconnpi1  35233  cvmsss2  35268  cvmlift2lem12  35308  satfv0  35352  satfv0fun  35365  satf00  35368  sat1el2xp  35373  fmla0xp  35377  fmlasucdisj  35393  satffunlem1lem1  35396  satffunlem2lem1  35398  dmopab3rexdif  35399  msubco  35525  msubvrs  35554  ellcsrspsn  35635  sinccvglem  35666  untsucf  35704  nnuni  35721  dfrdg2  35790  colineardim1  36056  btwnconn1lem14  36095  segleantisym  36110  colinbtwnle  36113  outsidele  36127  lineunray  36142  linethru  36148  elicc3  36312  opnregcld  36325  cldregopn  36326  fnejoin2  36364  bj-isrvec  37289  dissneqlem  37335  icorempo  37346  relowlssretop  37358  relowlpssretop  37359  rdgssun  37373  finxpsuclem  37392  lindsenlbs  37616  ptrecube  37621  poimirlem6  37627  poimirlem7  37628  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem21  37642  poimirlem22  37643  poimirlem23  37644  poimirlem24  37645  poimirlem25  37646  poimirlem26  37647  poimirlem27  37648  poimirlem29  37650  poimirlem30  37651  poimirlem31  37652  poimirlem32  37653  itg2addnclem3  37674  ftc1anclem6  37699  dvasin  37705  unirep  37715  sdclem2  37743  ssbnd  37789  prdsbnd  37794  cntotbnd  37797  heibor1lem  37810  rrnequiv  37836  ismndo2  37875  grpoeqdivid  37882  isdrngo3  37960  crngohomfo  38007  0idl  38026  1idl  38027  divrngidl  38029  smprngopr  38053  prnc  38068  ispridlc  38071  riotaclbgBAD  38954  lshpdisj  38987  lsateln0  38995  lsatcveq0  39032  opnlen0  39188  cmtbr4N  39255  cvrnbtwn2  39275  cvrnbtwn4  39279  atcvreq0  39314  cvlatexch1  39336  exatleN  39405  atlelt  39439  ps-2  39479  llnn0  39517  lplnn0N  39548  islpln2a  39549  lvoln0N  39592  islvol2aN  39593  4at  39614  dalemcea  39661  dalem3  39665  pmapglb2N  39772  pmapglb2xN  39773  cdlema1N  39792  cdlemb  39795  paddasslem17  39837  llnexchb2lem  39869  llnexchb2  39870  lhpat3  40047  ltrnid  40136  trlne  40186  cdlemc4  40195  cdleme11h  40267  cdlemednuN  40301  cdlemg1a  40571  tendoeq2  40775  tendoid0  40826  dva1dim  40986  dib1dim  41166  dihlatat  41338  dochkrshp4  41390  dochkr1  41479  lclkrlem2e  41512  lcfrlem16  41559  lcfrlem28  41571  mapd0  41666  hdmap14lem13  41881  eqresfnbd  42227  f1o2d2  42228  expeq1d  42319  expeqidd  42320  dvdsexpnn0  42329  reladdrsub  42380  sn-remul0ord  42403  sn-negex12  42412  sn-mullid  42431  sn-mul02  42447  nn0addcom  42457  nn0mulcom  42461  zmulcomlem  42462  mulgt0con1d  42465  mulgt0con2d  42466  sn-sup2  42486  frlmsnic  42535  evlselvlem  42581  prjspner1  42621  elrfi  42689  mrefg2  42702  eldiophb  42752  eldioph2b  42758  diophin  42767  diophun  42768  rexzrexnn0  42799  eldioph4b  42806  diophren  42808  rencldnfilem  42815  pellexlem6  42829  jm2.19  42989  rmydioph  43010  expdiophlem1  43017  expdioph  43019  lnr2i  43112  lpirlnr  43113  hbtlem2  43120  hbtlem4  43122  hbtlem6  43125  dgrsub2  43131  dgraa0p  43145  rngunsnply  43165  nlimsuc  43437  dfsucon  43519  radcnvrat  44310  pm14.24  44428  addrcom  44471  modelaxreplem1  44975  ormklocald  46879  natlocalincr  46881  afveu  47158  dfafn5b  47166  rlimdmafv  47182  afv2eu  47243  rlimdmafv2  47263  el1fzopredsuc  47330  minusmod5ne  47354  modmknepk  47367  elsetpreimafvssdm  47391  imasetpreimafvbijlemfo  47410  sprvalpw  47485  prprvalpw  47520  reupr  47527  fmtnofac2lem  47573  proththdlem  47618  perfectALTVlem2  47727  perfectALTV  47728  gbowpos  47764  gbowgt5  47767  gboge9  47769  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  uhgrimedgi  47894  isuspgrim0  47898  isuspgrimlem  47899  upgrimpths  47913  clnbgrgrim  47938  grimedg  47939  grtrissvtx  47947  stgredgiun  47961  stgrvtx0  47965  isubgr3stgrlem7  47975  grlimgrtrilem2  47998  gpgiedgdmellem  48041  gpgvtxel2  48043  gpgvtx0  48048  gpgvtx1  48049  gpgusgralem  48051  gpgedgvtx0  48056  gpgedgvtx1  48057  gpgedg2ov  48061  gpgedg2iv  48062  gpgnbgrvtx0  48069  gpgnbgrvtx1  48070  pgnbgreunbgr  48119  ringcinvALTV  48302  lincellss  48419  lindsrng01  48461  suppdm  48503  nnpw2pb  48580  0aryfvalel  48627  0aryfvalelfv  48628  itsclc0xyqsolr  48762  infsubc  49053  infsubc2  49054