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  4488  elsn2g  4617  preq1b  4798  elpreqprb  4820  reusv3  5343  alxfr  5345  reuhypd  5357  axpr  5365  opth1  5415  euotd  5453  otiunsndisj  5460  tz7.2  5599  frsn  5704  dmopab2rex  5857  elsnxp  6238  reuop  6240  dfpo2  6243  ordtri1  6339  ordtri3  6342  fvmptdv2  6947  fveqressseq  7012  foco2  7042  fsn  7068  fnsnbg  7098  fnsnbOLD  7100  fmptsng  7102  fmptsnd  7103  fconst2g  7137  fnprb  7142  fntpb  7143  funfvima  7164  soisoi  7262  isores3  7269  eqfunresadj  7294  riotaeqimp  7329  eusvobj2  7338  ovmpodv2  7504  f1opw2  7601  sorpssun  7663  sorpssin  7664  oneqmin  7733  nlimsucg  7772  onzsl  7776  tfinds  7790  funcnvuni  7862  mptcnfimad  7918  opiota  7991  mposn  8033  frpoins3xpg  8070  frpoins3xp3g  8071  poxp2  8073  xpord2pred  8075  sexp2  8076  poxp3  8080  xpord3pred  8082  sexp3  8083  xpord3inddlem  8084  suppssov1  8127  suppssov2  8128  suppssfv  8132  brtpos  8165  frrlem12  8227  frrlem13  8228  seqomlem1  8369  seqomlem2  8370  omordi  8481  omord  8483  omwordi  8486  oeeui  8517  nnmordi  8546  nnmord  8547  nnmwordi  8550  nnawordex  8552  nnaordex  8553  nneob  8571  omsmolem  8572  eldifsucnn  8579  qsss  8700  eroveu  8736  mapsncnv  8817  ralxpmap  8820  elixpsn  8861  ixpsnf1o  8862  boxcutc  8865  pw2f1olem  8994  2pwne  9046  mapxpen  9056  mapunen  9059  php  9116  onomeneq  9123  unxpdomlem2  9141  en1eqsnbi  9160  isfiniteg  9184  fofinf1o  9216  f1opwfi  9240  elfiun  9314  oieu  9425  brwdom2  9459  wdomtr  9461  ixpiunwdom  9476  en3lplem1  9502  suc11reg  9509  inf3lemd  9517  cantnfvalf  9555  cantnflt  9562  cantnfp1lem3  9570  cantnflem2  9580  ttrcltr  9606  rnttrcl  9612  ttrclselem1  9615  r1tr  9669  updjud  9827  dfac8alem  9920  wdomnumr  9955  isinfcard  9983  aceq3lem  10011  dfac5lem4  10017  dfac5lem4OLD  10019  dfac5  10020  dfac2b  10022  coftr  10164  fin23lem28  10231  fin23lem29  10232  fin1a2lem11  10301  fin1a2lem12  10302  fin1a2lem13  10303  hsmexlem9  10316  axdclem  10410  pwcfsdom  10474  gchdomtri  10520  fpwwe2  10534  gchpwdom  10561  gchhar  10570  addnidpi  10792  nqereu  10820  genpv  10890  genpdm  10893  distrlem5pr  10918  mulrid  11110  ltne  11210  mul02  11291  cnegex  11294  mul0or  11757  negfi  12071  sup2  12078  supaddc  12089  supadd  12090  supmul1  12091  supmul  12094  creur  12119  creui  12120  cju  12121  nnsub  12169  un0addcl  12414  un0mulcl  12415  nn0sub  12431  elz2  12486  zaddcl  12512  suprzcl2  12836  qmulz  12849  qre  12851  qnegcl  12864  elpqb  12874  xrmax1  13074  xrmin2  13077  max1ALT  13085  xlesubadd  13162  xmulass  13186  xlemul1a  13187  xrsupexmnf  13204  xrinfmexpnf  13205  xrub  13211  iccid  13290  fzsn  13466  fzsuc2  13482  fz1sbc  13500  elfzp12  13503  modmuladd  13820  seqid3  13953  bcval5  14225  bcpasc  14228  hashbnd  14243  hashnnn0genn0  14250  hashprg  14302  hashfzo  14336  tpfo  14407  wrdl1s1  14522  ccats1alpha  14527  cats1un  14628  s7f1o  14873  shftlem  14975  replim  15023  absmod0  15210  absz  15218  rlimdm  15458  summolem2  15623  summo  15624  zsum  15625  fsum  15627  fsummulc2  15691  fsumconst  15697  fsum00  15705  incexclem  15743  isumsplit  15747  infcvgaux1i  15764  prodmolem2  15842  prodmo  15843  zprod  15844  fprod  15848  prodsn  15869  prodsnf  15871  fprodconst  15885  ruclem2  16141  fzo0dvdseq  16234  bitsf1ocnv  16355  sadcaddlem  16368  smueqlem  16401  gcdabs1  16440  bezoutlem1  16450  bezoutlem3  16452  bezoutlem4  16453  dvdsgcd  16455  dvdsmulgcd  16467  lcmgcdeq  16523  lcmf  16544  lcmfunsnlem1  16548  lcmfunsnlem2lem2  16550  isprm2lem  16592  dvdsprime  16598  isprm5  16618  coprm  16622  prmdvdsexpr  16628  rpexp  16633  phibndlem  16681  dfphi2  16685  hashgcdlem  16699  odzdvds  16707  nnoddn2prm  16723  pythagtriplem1  16728  iserodd  16747  pceulem  16757  pcqmul  16765  pcqcl  16768  pcxnn0cl  16772  pcxcl  16773  pcneg  16786  pcabs  16787  pcgcd1  16789  pcz  16793  pcprmpw2  16794  pcprmpw  16795  dvdsprmpweqle  16798  difsqpwdvds  16799  pcaddlem  16800  pcadd  16801  pcmpt  16804  pockthg  16818  prmreclem5  16832  4sqlem4  16864  mul4sq  16866  vdwapun  16886  vdwlem2  16894  vdwlem6  16898  vdwlem8  16900  vdwlem13  16905  0ram  16932  ram0  16934  ramcl  16941  cshwsiun  17011  wunress  17160  firest  17336  isssc  17727  pospo  18249  latnlej  18362  gsumval2a  18593  xpsmnd0  18686  mnd1id  18688  0subm  18725  mulgnn0p1  18998  mulgnn0ass  19023  cyccom  19116  gicsubgen  19192  symg1bas  19304  snsymgefmndeq  19308  psgnunilem1  19406  psgnunilem2  19408  mndodcongi  19456  oddvdsnn0  19457  odnncl  19458  oddvds  19460  odeq  19463  odeq1  19473  pgpfi2  19519  sylow2a  19532  sylow2blem3  19535  sylow3lem6  19545  lsmelvalm  19564  lsmsubm  19566  lsmsubg  19567  lsmmod  19588  lsmdisj2  19595  efgmnvl  19627  efgtlen  19639  efgs1b  19649  efgrelexlemb  19663  efgredeu  19665  efgcpbllemb  19668  frgpuptinv  19684  frgpup3lem  19690  qusabl  19778  frgpnabllem1  19786  cyggeninv  19796  cyggenod  19797  gsumval3eu  19817  dprdssv  19931  dprdfeq0  19937  dprdsubg  19939  dprddisj2  19954  ablfacrp  19981  pgpfac1lem3  19992  pgpfaclem2  19997  xpsring1d  20252  dvreq1  20330  irredn1  20345  nzrunit  20440  ringcinv  20587  rrgeq0  20616  domneq0  20624  drngmul0orOLD  20677  isabvd  20728  abvdom  20746  issrngd  20771  lmodfopnelem2  20833  lss1d  20897  lspsneq0  20946  lbspss  21017  lsmcl  21018  lvecvs0or  21046  lspindpi  21070  lidl1el  21164  lpiss  21267  lidldvgen  21272  qsssubdrg  21364  zringlpirlem1  21400  pzriprnglem6  21424  pzriprnglem12  21430  znfld  21498  znunit  21501  znrrg  21503  cygznlem3  21507  frgpcyg  21511  psgnghm  21518  ipeq0  21576  cssincl  21626  lsmcss  21630  obselocv  21666  dsmmacl  21679  dsmmlss  21682  mplsubrglem  21942  mplmonmul  21972  mplcoe5lem  21975  mhpsclcl  22063  mhpvarcl  22064  psdmul  22082  coe1tmmul2  22191  coe1tmmul  22192  pf1ind  22271  mat1dimelbas  22387  mdetralt  22524  mdetunilem2  22529  mdetunilem7  22534  mdetunilem9  22536  maducoeval2  22556  chpscmat  22758  chfacfscmulgsum  22776  chfacfpmmulgsum  22780  istopon  22828  eltg3  22878  tgidm  22896  clsval2  22966  opncldf1  23000  restbas  23074  tgrest  23075  restcld  23088  restcldr  23090  restcls  23097  restntr  23098  ordtbas2  23107  ordtbas  23108  ordtrest2lem  23119  ordtrest2  23120  pnfnei  23136  mnfnei  23137  tgcn  23168  cnconst  23200  cnindis  23208  lmss  23214  ordtt1  23295  discmp  23314  1stcrest  23369  2ndcdisj  23372  cldllycmp  23411  txbas  23483  ptpjpre1  23487  ptuni2  23492  ptbasin  23493  ptbasfi  23497  ptopn2  23500  txbasval  23522  ptpjopn  23528  ptclsg  23531  dfac14lem  23533  xkoccn  23535  ptcnp  23538  upxp  23539  ptrescn  23555  txkgen  23568  xkoptsub  23570  xkopt  23571  xkoco1cn  23573  xkoco2cn  23574  xkococn  23576  xkoinjcn  23603  ordthmeolem  23717  ptuncnv  23723  nrmhaus  23742  fbssint  23754  fbfinnfr  23757  fbasrn  23800  isufil2  23824  filufint  23836  rnelfm  23869  fmfnfmlem2  23871  fmfnfmlem3  23872  fmfnfmlem4  23873  fmfnfm  23874  flimtopon  23886  flimclslem  23900  fclstopon  23928  fclscf  23941  flimfnfcls  23944  alexsublem  23960  alexsubALTlem3  23965  alexsubALTlem4  23966  ptcmplem2  23969  tmdgsum2  24012  symgtgp  24022  cldsubg  24027  qustgplem  24037  tgptsmscld  24067  tsmsxplem1  24069  imasdsf1olem  24289  blssps  24340  blss  24341  stdbdxmet  24431  methaus  24436  metrest  24440  nrginvrcn  24608  nmoeq0  24652  blssioo  24711  xrtgioo  24723  xrsxmet  24726  reconnlem1  24743  reconnlem2  24744  xrge0tsms  24751  elcncf1di  24816  iccpnfcnv  24870  evth  24886  lebnumlem1  24888  lebnumlem2  24889  lebnumlem3  24890  nmoleub3  25047  minveclem3b  25356  ivthlem2  25381  ivthlem3  25382  elovolm  25404  ovolmge0  25406  ovoliun  25434  ovolicc2lem3  25448  ovolicc2  25451  voliunlem3  25481  dyaddisj  25525  dyadmax  25527  opnmblALT  25532  ismbfd  25568  ismbf2d  25569  mbfimaopnlem  25584  mbfimaopn2  25586  i1fmullem  25623  i1fres  25634  itg1climres  25643  mbfi1fseqlem4  25647  itg2lcl  25656  itgsplitioo  25767  ellimc2  25806  rolle  25922  dvlip  25926  dvge0  25939  dvne0  25944  lhop1lem  25946  tdeglem4  25993  degltlem1  26005  deg1nn0clb  26023  deg1lt0  26024  dvdsq1p  26096  ply1rem  26099  fta1g  26103  elply2  26129  plyf  26131  ne0p  26140  plyeq0lem  26143  plypf1  26145  0dgrb  26179  coe1termlem  26191  dgrcolem2  26208  plymul0or  26216  plyrem  26241  fta1  26244  quotcan  26245  aalioulem3  26270  eff1olem  26485  lognegb  26527  eflogeq  26539  argregt0  26547  argrege0  26548  tanarg  26556  cxpexp  26605  cxpeq0  26615  mulcxp  26622  cxpeq  26695  atans2  26869  scvxcvx  26924  dmgmaddn0  26961  isppw2  27053  vmappw  27054  vmacl  27056  efvmacl  27058  isnsqf  27073  mumullem2  27118  sqff1o  27120  dvdsppwf1o  27124  ppiublem1  27141  vmalelog  27144  chtublem  27150  fsumvma  27152  perfectlem2  27169  perfect  27170  bposlem1  27223  lgsmod  27262  lgsne0  27274  lgsdirnn0  27283  lgsqr  27290  lgsdchr  27294  gausslemma2dlem1a  27304  gausslemma2dlem6  27311  lgseisenlem2  27315  lgsquadlem1  27319  lgsquadlem2  27320  2lgslem1b  27331  2sqlem2  27357  mul2sq  27358  2sqlem7  27363  dchrisum0fno1  27450  pntrsumbnd2  27506  ostthlem1  27566  ostth2lem2  27573  ostth3  27577  ostth  27578  nolesgn2ores  27612  nogesgn1ores  27614  nolt02o  27635  nogt01o  27636  nosupbnd2  27656  noinfbnd2lem1  27670  noetasuplem4  27676  noetainflem4  27680  maxs1  27705  mins2  27708  sltne  27710  eqscut3  27766  cuteq1  27779  madef  27798  sltlpss  27854  lrrecfr  27887  addsval  27906  addsproplem2  27914  addsuniflem  27945  addsbdaylem  27960  negsid  27984  negsunif  27998  mulsproplem5  28060  mulsproplem6  28061  mulsproplem7  28062  mulsproplem8  28063  mulsproplem9  28064  slemuld  28078  ssltmul1  28087  ssltmul2  28088  sltmul2  28111  muls0ord  28125  precsexlem8  28153  precsexlem9  28154  precsexlem11  28156  elons2  28196  onscutlt  28202  bdayon  28210  onaddscl  28211  onmulscl  28212  nnsge1  28272  n0sfincut  28283  n0subs  28290  dfnns2  28298  eucliddivs  28302  znegscl  28317  zaddscl  28319  zmulscld  28322  elzn0s  28323  eln0zs  28325  n0seo  28345  zseo  28346  zs12no  28387  zs12addscl  28388  zs12negscl  28389  zs12half  28391  zs12zodd  28393  zs12ge0  28394  zs12bday  28395  recut  28399  0reno  28400  remulscllem1  28403  colinearalg  28889  axpasch  28920  axlowdimlem16  28936  axlowdimlem17  28937  axlowdim  28940  axcontlem2  28944  axcontlem4  28946  axcontlem7  28949  lpvtx  29047  edglnl  29122  numedglnl  29123  usgredgop  29149  usgrexmplef  29238  uhgrspansubgrlem  29269  uhgrspan1  29282  nbusgredgeu0  29347  nb3grprlem2  29360  cusgrsize2inds  29433  vtxd0nedgb  29468  rusgrpropnb  29563  upgrwlkvtxedg  29624  wlkp1lem1  29651  wlkp1lem6  29656  wlkp1lem8  29658  usgr2wlkneq  29735  crctcshwlk  29801  crctcsh  29803  iswwlksnon  29832  wlkiswwlks1  29846  wwlksnextbi  29873  wwlksnextproplem2  29889  wspthsnonn0vne  29896  clwlkclwwlklem2  29978  clwwisshclwws  29993  erclwwlktr  30000  clwwlkel  30024  clwwlkext2edg  30034  erclwwlkntr  30049  clwlknf1oclwwlknlem2  30060  clwlknf1oclwwlknlem3  30061  clwlknf1oclwwlkn  30062  clwwlknonccat  30074  0wlkons1  30099  3wlkdlem6  30143  eupth2eucrct  30195  frgrwopreglem2  30291  2clwwlk2clwwlk  30328  wlkl0  30345  nvmul0or  30628  ipasslem5  30813  ipasslem11  30818  hvmul0or  31003  his6  31077  hhssnv  31242  ocsh  31261  ocin  31274  shsidmi  31362  chnlen0  31422  h1de2bi  31532  h1de2ctlem  31533  h1de2ci  31534  spansni  31535  3oalem1  31640  nmcexi  32004  atcveq0  32326  chcv1  32333  cdjreui  32410  cdj3lem2b  32415  xrge0tsmsd  33040  1fldgenq  33286  ccfldextdgrr  33683  ordtrest2NEWlem  33933  ordtrest2NEW  33934  xrge0iifcnv  33944  esumc  34062  esumpcvgval  34089  ballotlemfc0  34504  ballotlemfcc  34505  fissorduni  35099  fineqvnttrclse  35142  gblacfnacd  35144  subfacp1lem4  35225  subfacp1lem5  35226  erdszelem8  35240  sconnpi1  35281  cvmsss2  35316  cvmlift2lem12  35356  satfv0  35400  satfv0fun  35413  satf00  35416  sat1el2xp  35421  fmla0xp  35425  fmlasucdisj  35441  satffunlem1lem1  35444  satffunlem2lem1  35446  dmopab3rexdif  35447  msubco  35573  msubvrs  35602  ellcsrspsn  35683  sinccvglem  35714  untsucf  35752  nnuni  35769  dfrdg2  35835  colineardim1  36101  btwnconn1lem14  36140  segleantisym  36155  colinbtwnle  36158  outsidele  36172  lineunray  36187  linethru  36193  elicc3  36357  opnregcld  36370  cldregopn  36371  fnejoin2  36409  bj-isrvec  37334  dissneqlem  37380  icorempo  37391  relowlssretop  37403  relowlpssretop  37404  rdgssun  37418  finxpsuclem  37437  lindsenlbs  37661  ptrecube  37666  poimirlem6  37672  poimirlem7  37673  poimirlem16  37682  poimirlem17  37683  poimirlem19  37685  poimirlem20  37686  poimirlem21  37687  poimirlem22  37688  poimirlem23  37689  poimirlem24  37690  poimirlem25  37691  poimirlem26  37692  poimirlem27  37693  poimirlem29  37695  poimirlem30  37696  poimirlem31  37697  poimirlem32  37698  itg2addnclem3  37719  ftc1anclem6  37744  dvasin  37750  unirep  37760  sdclem2  37788  ssbnd  37834  prdsbnd  37839  cntotbnd  37842  heibor1lem  37855  rrnequiv  37881  ismndo2  37920  grpoeqdivid  37927  isdrngo3  38005  crngohomfo  38052  0idl  38071  1idl  38072  divrngidl  38074  smprngopr  38098  prnc  38113  ispridlc  38116  riotaclbgBAD  38999  lshpdisj  39032  lsateln0  39040  lsatcveq0  39077  opnlen0  39233  cmtbr4N  39300  cvrnbtwn2  39320  cvrnbtwn4  39324  atcvreq0  39359  cvlatexch1  39381  exatleN  39449  atlelt  39483  ps-2  39523  llnn0  39561  lplnn0N  39592  islpln2a  39593  lvoln0N  39636  islvol2aN  39637  4at  39658  dalemcea  39705  dalem3  39709  pmapglb2N  39816  pmapglb2xN  39817  cdlema1N  39836  cdlemb  39839  paddasslem17  39881  llnexchb2lem  39913  llnexchb2  39914  lhpat3  40091  ltrnid  40180  trlne  40230  cdlemc4  40239  cdleme11h  40311  cdlemednuN  40345  cdlemg1a  40615  tendoeq2  40819  tendoid0  40870  dva1dim  41030  dib1dim  41210  dihlatat  41382  dochkrshp4  41434  dochkr1  41523  lclkrlem2e  41556  lcfrlem16  41603  lcfrlem28  41615  mapd0  41710  hdmap14lem13  41925  eqresfnbd  42271  f1o2d2  42272  expeq1d  42363  expeqidd  42364  dvdsexpnn0  42373  reladdrsub  42424  sn-remul0ord  42447  sn-negex12  42456  sn-mullid  42475  sn-mul02  42491  nn0addcom  42501  nn0mulcom  42505  zmulcomlem  42506  mulgt0con1d  42509  mulgt0con2d  42510  sn-sup2  42530  frlmsnic  42579  evlselvlem  42625  prjspner1  42665  elrfi  42733  mrefg2  42746  eldiophb  42796  eldioph2b  42802  diophin  42811  diophun  42812  rexzrexnn0  42843  eldioph4b  42850  diophren  42852  rencldnfilem  42859  pellexlem6  42873  jm2.19  43032  rmydioph  43053  expdiophlem1  43060  expdioph  43062  lnr2i  43155  lpirlnr  43156  hbtlem2  43163  hbtlem4  43165  hbtlem6  43168  dgrsub2  43174  dgraa0p  43188  rngunsnply  43208  nlimsuc  43480  dfsucon  43562  radcnvrat  44353  pm14.24  44471  addrcom  44513  modelaxreplem1  45017  ormklocald  46918  natlocalincr  46920  afveu  47190  dfafn5b  47198  rlimdmafv  47214  afv2eu  47275  rlimdmafv2  47295  el1fzopredsuc  47362  minusmod5ne  47386  modmknepk  47399  elsetpreimafvssdm  47423  imasetpreimafvbijlemfo  47442  sprvalpw  47517  prprvalpw  47552  reupr  47559  fmtnofac2lem  47605  proththdlem  47650  perfectALTVlem2  47759  perfectALTV  47760  gbowpos  47796  gbowgt5  47799  gboge9  47801  nnsum4primesodd  47833  nnsum4primesoddALTV  47834  uhgrimedgi  47927  isuspgrim0  47931  isuspgrimlem  47932  upgrimpths  47946  clnbgrgrim  47971  grimedg  47972  grtrissvtx  47981  stgredgiun  47995  stgrvtx0  47999  isubgr3stgrlem7  48009  grlimgrtrilem2  48039  gpgiedgdmellem  48083  gpgvtxel2  48085  gpgvtx0  48090  gpgvtx1  48091  gpgusgralem  48093  gpgedgvtx0  48098  gpgedgvtx1  48099  gpgedg2ov  48103  gpgedg2iv  48104  gpgnbgrvtx0  48111  gpgnbgrvtx1  48112  pgnbgreunbgr  48162  ringcinvALTV  48347  lincellss  48464  lindsrng01  48506  suppdm  48548  nnpw2pb  48625  0aryfvalel  48672  0aryfvalelfv  48673  itsclc0xyqsolr  48807  infsubc  49098  infsubc2  49099