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  4491  elsn2g  4618  preq1b  4800  elpreqprb  4822  reusv3  5347  alxfr  5349  reuhypd  5361  axpr  5369  opth1  5422  euotd  5460  otiunsndisj  5467  tz7.2  5606  frsn  5711  dmopab2rex  5864  elsnxp  6243  reuop  6245  dfpo2  6248  ordtri1  6344  ordtri3  6347  fvmptdv2  6952  fveqressseq  7017  foco2  7047  fsn  7073  fnsnbg  7104  fnsnbOLD  7106  fmptsng  7108  fmptsnd  7109  fconst2g  7143  fnprb  7148  fntpb  7149  funfvima  7170  soisoi  7269  isores3  7276  eqfunresadj  7301  riotaeqimp  7336  eusvobj2  7345  ovmpodv2  7511  f1opw2  7608  sorpssun  7670  sorpssin  7671  oneqmin  7740  nlimsucg  7782  onzsl  7786  tfinds  7800  funcnvuni  7872  mptcnfimad  7928  opiota  8001  mposn  8043  frpoins3xpg  8080  frpoins3xp3g  8081  poxp2  8083  xpord2pred  8085  sexp2  8086  poxp3  8090  xpord3pred  8092  sexp3  8093  xpord3inddlem  8094  suppssov1  8137  suppssov2  8138  suppssfv  8142  brtpos  8175  frrlem12  8237  frrlem13  8238  seqomlem1  8379  seqomlem2  8380  omordi  8491  omord  8493  omwordi  8496  oeeui  8527  nnmordi  8556  nnmord  8557  nnmwordi  8560  nnawordex  8562  nnaordex  8563  nneob  8581  omsmolem  8582  eldifsucnn  8589  qsss  8710  eroveu  8746  mapsncnv  8827  ralxpmap  8830  elixpsn  8871  ixpsnf1o  8872  boxcutc  8875  pw2f1olem  9005  2pwne  9057  mapxpen  9067  mapunen  9070  php  9131  onomeneq  9138  unxpdomlem2  9156  en1eqsnbi  9179  isfiniteg  9206  fofinf1o  9241  f1opwfi  9265  elfiun  9339  oieu  9450  brwdom2  9484  wdomtr  9486  ixpiunwdom  9501  en3lplem1  9527  suc11reg  9534  inf3lemd  9542  cantnfvalf  9580  cantnflt  9587  cantnfp1lem3  9595  cantnflem2  9605  ttrcltr  9631  rnttrcl  9637  ttrclselem1  9640  r1tr  9691  updjud  9849  dfac8alem  9942  wdomnumr  9977  isinfcard  10005  aceq3lem  10033  dfac5lem4  10039  dfac5lem4OLD  10041  dfac5  10042  dfac2b  10044  coftr  10186  fin23lem28  10253  fin23lem29  10254  fin1a2lem11  10323  fin1a2lem12  10324  fin1a2lem13  10325  hsmexlem9  10338  axdclem  10432  pwcfsdom  10496  gchdomtri  10542  fpwwe2  10556  gchpwdom  10583  gchhar  10592  addnidpi  10814  nqereu  10842  genpv  10912  genpdm  10915  distrlem5pr  10940  mulrid  11132  ltne  11231  mul02  11312  cnegex  11315  mul0or  11778  negfi  12092  sup2  12099  supaddc  12110  supadd  12111  supmul1  12112  supmul  12115  creur  12140  creui  12141  cju  12142  nnsub  12190  un0addcl  12435  un0mulcl  12436  nn0sub  12452  elz2  12507  zaddcl  12533  suprzcl2  12857  qmulz  12870  qre  12872  qnegcl  12885  elpqb  12895  xrmax1  13095  xrmin2  13098  max1ALT  13106  xlesubadd  13183  xmulass  13207  xlemul1a  13208  xrsupexmnf  13225  xrinfmexpnf  13226  xrub  13232  iccid  13311  fzsn  13487  fzsuc2  13503  fz1sbc  13521  elfzp12  13524  modmuladd  13838  seqid3  13971  bcval5  14243  bcpasc  14246  hashbnd  14261  hashnnn0genn0  14268  hashprg  14320  hashfzo  14354  tpfo  14425  wrdl1s1  14539  ccats1alpha  14544  cats1un  14645  s7f1o  14891  shftlem  14993  replim  15041  absmod0  15228  absz  15236  rlimdm  15476  summolem2  15641  summo  15642  zsum  15643  fsum  15645  fsummulc2  15709  fsumconst  15715  fsum00  15723  incexclem  15761  isumsplit  15765  infcvgaux1i  15782  prodmolem2  15860  prodmo  15861  zprod  15862  fprod  15866  prodsn  15887  prodsnf  15889  fprodconst  15903  ruclem2  16159  fzo0dvdseq  16252  bitsf1ocnv  16373  sadcaddlem  16386  smueqlem  16419  gcdabs1  16458  bezoutlem1  16468  bezoutlem3  16470  bezoutlem4  16471  dvdsgcd  16473  dvdsmulgcd  16485  lcmgcdeq  16541  lcmf  16562  lcmfunsnlem1  16566  lcmfunsnlem2lem2  16568  isprm2lem  16610  dvdsprime  16616  isprm5  16636  coprm  16640  prmdvdsexpr  16646  rpexp  16651  phibndlem  16699  dfphi2  16703  hashgcdlem  16717  odzdvds  16725  nnoddn2prm  16741  pythagtriplem1  16746  iserodd  16765  pceulem  16775  pcqmul  16783  pcqcl  16786  pcxnn0cl  16790  pcxcl  16791  pcneg  16804  pcabs  16805  pcgcd1  16807  pcz  16811  pcprmpw2  16812  pcprmpw  16813  dvdsprmpweqle  16816  difsqpwdvds  16817  pcaddlem  16818  pcadd  16819  pcmpt  16822  pockthg  16836  prmreclem5  16850  4sqlem4  16882  mul4sq  16884  vdwapun  16904  vdwlem2  16912  vdwlem6  16916  vdwlem8  16918  vdwlem13  16923  0ram  16950  ram0  16952  ramcl  16959  cshwsiun  17029  wunress  17178  firest  17354  isssc  17745  pospo  18267  latnlej  18380  gsumval2a  18577  xpsmnd0  18670  mnd1id  18672  0subm  18709  mulgnn0p1  18982  mulgnn0ass  19007  cyccom  19100  gicsubgen  19176  symg1bas  19288  snsymgefmndeq  19292  psgnunilem1  19390  psgnunilem2  19392  mndodcongi  19440  oddvdsnn0  19441  odnncl  19442  oddvds  19444  odeq  19447  odeq1  19457  pgpfi2  19503  sylow2a  19516  sylow2blem3  19519  sylow3lem6  19529  lsmelvalm  19548  lsmsubm  19550  lsmsubg  19551  lsmmod  19572  lsmdisj2  19579  efgmnvl  19611  efgtlen  19623  efgs1b  19633  efgrelexlemb  19647  efgredeu  19649  efgcpbllemb  19652  frgpuptinv  19668  frgpup3lem  19674  qusabl  19762  frgpnabllem1  19770  cyggeninv  19780  cyggenod  19781  gsumval3eu  19801  dprdssv  19915  dprdfeq0  19921  dprdsubg  19923  dprddisj2  19938  ablfacrp  19965  pgpfac1lem3  19976  pgpfaclem2  19981  xpsring1d  20236  dvreq1  20314  irredn1  20329  nzrunit  20427  ringcinv  20574  rrgeq0  20603  domneq0  20611  drngmul0orOLD  20664  isabvd  20715  abvdom  20733  issrngd  20758  lmodfopnelem2  20820  lss1d  20884  lspsneq0  20933  lbspss  21004  lsmcl  21005  lvecvs0or  21033  lspindpi  21057  lidl1el  21151  lpiss  21254  lidldvgen  21259  qsssubdrg  21351  zringlpirlem1  21387  pzriprnglem6  21411  pzriprnglem12  21417  znfld  21485  znunit  21488  znrrg  21490  cygznlem3  21494  frgpcyg  21498  psgnghm  21505  ipeq0  21563  cssincl  21613  lsmcss  21617  obselocv  21653  dsmmacl  21666  dsmmlss  21669  mplsubrglem  21929  mplmonmul  21959  mplcoe5lem  21962  mhpsclcl  22050  mhpvarcl  22051  psdmul  22069  coe1tmmul2  22178  coe1tmmul  22179  pf1ind  22258  mat1dimelbas  22374  mdetralt  22511  mdetunilem2  22516  mdetunilem7  22521  mdetunilem9  22523  maducoeval2  22543  chpscmat  22745  chfacfscmulgsum  22763  chfacfpmmulgsum  22767  istopon  22815  eltg3  22865  tgidm  22883  clsval2  22953  opncldf1  22987  restbas  23061  tgrest  23062  restcld  23075  restcldr  23077  restcls  23084  restntr  23085  ordtbas2  23094  ordtbas  23095  ordtrest2lem  23106  ordtrest2  23107  pnfnei  23123  mnfnei  23124  tgcn  23155  cnconst  23187  cnindis  23195  lmss  23201  ordtt1  23282  discmp  23301  1stcrest  23356  2ndcdisj  23359  cldllycmp  23398  txbas  23470  ptpjpre1  23474  ptuni2  23479  ptbasin  23480  ptbasfi  23484  ptopn2  23487  txbasval  23509  ptpjopn  23515  ptclsg  23518  dfac14lem  23520  xkoccn  23522  ptcnp  23525  upxp  23526  ptrescn  23542  txkgen  23555  xkoptsub  23557  xkopt  23558  xkoco1cn  23560  xkoco2cn  23561  xkococn  23563  xkoinjcn  23590  ordthmeolem  23704  ptuncnv  23710  nrmhaus  23729  fbssint  23741  fbfinnfr  23744  fbasrn  23787  isufil2  23811  filufint  23823  rnelfm  23856  fmfnfmlem2  23858  fmfnfmlem3  23859  fmfnfmlem4  23860  fmfnfm  23861  flimtopon  23873  flimclslem  23887  fclstopon  23915  fclscf  23928  flimfnfcls  23931  alexsublem  23947  alexsubALTlem3  23952  alexsubALTlem4  23953  ptcmplem2  23956  tmdgsum2  23999  symgtgp  24009  cldsubg  24014  qustgplem  24024  tgptsmscld  24054  tsmsxplem1  24056  imasdsf1olem  24277  blssps  24328  blss  24329  stdbdxmet  24419  methaus  24424  metrest  24428  nrginvrcn  24596  nmoeq0  24640  blssioo  24699  xrtgioo  24711  xrsxmet  24714  reconnlem1  24731  reconnlem2  24732  xrge0tsms  24739  elcncf1di  24804  iccpnfcnv  24858  evth  24874  lebnumlem1  24876  lebnumlem2  24877  lebnumlem3  24878  nmoleub3  25035  minveclem3b  25344  ivthlem2  25369  ivthlem3  25370  elovolm  25392  ovolmge0  25394  ovoliun  25422  ovolicc2lem3  25436  ovolicc2  25439  voliunlem3  25469  dyaddisj  25513  dyadmax  25515  opnmblALT  25520  ismbfd  25556  ismbf2d  25557  mbfimaopnlem  25572  mbfimaopn2  25574  i1fmullem  25611  i1fres  25622  itg1climres  25631  mbfi1fseqlem4  25635  itg2lcl  25644  itgsplitioo  25755  ellimc2  25794  rolle  25910  dvlip  25914  dvge0  25927  dvne0  25932  lhop1lem  25934  tdeglem4  25981  degltlem1  25993  deg1nn0clb  26011  deg1lt0  26012  dvdsq1p  26084  ply1rem  26087  fta1g  26091  elply2  26117  plyf  26119  ne0p  26128  plyeq0lem  26131  plypf1  26133  0dgrb  26167  coe1termlem  26179  dgrcolem2  26196  plymul0or  26204  plyrem  26229  fta1  26232  quotcan  26233  aalioulem3  26258  eff1olem  26473  lognegb  26515  eflogeq  26527  argregt0  26535  argrege0  26536  tanarg  26544  cxpexp  26593  cxpeq0  26603  mulcxp  26610  cxpeq  26683  atans2  26857  scvxcvx  26912  dmgmaddn0  26949  isppw2  27041  vmappw  27042  vmacl  27044  efvmacl  27046  isnsqf  27061  mumullem2  27106  sqff1o  27108  dvdsppwf1o  27112  ppiublem1  27129  vmalelog  27132  chtublem  27138  fsumvma  27140  perfectlem2  27157  perfect  27158  bposlem1  27211  lgsmod  27250  lgsne0  27262  lgsdirnn0  27271  lgsqr  27278  lgsdchr  27282  gausslemma2dlem1a  27292  gausslemma2dlem6  27299  lgseisenlem2  27303  lgsquadlem1  27307  lgsquadlem2  27308  2lgslem1b  27319  2sqlem2  27345  mul2sq  27346  2sqlem7  27351  dchrisum0fno1  27438  pntrsumbnd2  27494  ostthlem1  27554  ostth2lem2  27561  ostth3  27565  ostth  27566  nolesgn2ores  27600  nogesgn1ores  27602  nolt02o  27623  nogt01o  27624  nosupbnd2  27644  noinfbnd2lem1  27658  noetasuplem4  27664  noetainflem4  27668  maxs1  27693  mins2  27696  sltne  27698  ssltsn  27721  eqscut3  27753  cuteq1  27766  madef  27784  sltlpss  27840  lrrecfr  27873  addsval  27892  addsproplem2  27900  addsuniflem  27931  addsbdaylem  27946  negsid  27970  negsunif  27984  mulsproplem5  28046  mulsproplem6  28047  mulsproplem7  28048  mulsproplem8  28049  mulsproplem9  28050  slemuld  28064  ssltmul1  28073  ssltmul2  28074  sltmul2  28097  muls0ord  28111  precsexlem8  28139  precsexlem9  28140  precsexlem11  28142  elons2  28182  onscutlt  28188  bdayon  28196  onaddscl  28197  onmulscl  28198  nnsge1  28258  n0sfincut  28269  n0subs  28276  dfnns2  28284  eucliddivs  28288  znegscl  28303  zaddscl  28305  zmulscld  28308  elzn0s  28309  eln0zs  28311  n0seo  28331  zseo  28332  zs12no  28371  zs12addscl  28372  zs12negscl  28373  zs12half  28375  zs12zodd  28377  zs12ge0  28378  zs12bday  28379  recut  28383  0reno  28384  remulscllem1  28387  colinearalg  28873  axpasch  28904  axlowdimlem16  28920  axlowdimlem17  28921  axlowdim  28924  axcontlem2  28928  axcontlem4  28930  axcontlem7  28933  lpvtx  29031  edglnl  29106  numedglnl  29107  usgredgop  29133  usgrexmplef  29222  uhgrspansubgrlem  29253  uhgrspan1  29266  nbusgredgeu0  29331  nb3grprlem2  29344  cusgrsize2inds  29417  vtxd0nedgb  29452  rusgrpropnb  29547  upgrwlkvtxedg  29608  wlkp1lem1  29635  wlkp1lem6  29640  wlkp1lem8  29642  usgr2wlkneq  29719  crctcshwlk  29785  crctcsh  29787  iswwlksnon  29816  wlkiswwlks1  29830  wwlksnextbi  29857  wwlksnextproplem2  29873  wspthsnonn0vne  29880  clwlkclwwlklem2  29962  clwwisshclwws  29977  erclwwlktr  29984  clwwlkel  30008  clwwlkext2edg  30018  erclwwlkntr  30033  clwlknf1oclwwlknlem2  30044  clwlknf1oclwwlknlem3  30045  clwlknf1oclwwlkn  30046  clwwlknonccat  30058  0wlkons1  30083  3wlkdlem6  30127  eupth2eucrct  30179  frgrwopreglem2  30275  2clwwlk2clwwlk  30312  wlkl0  30329  nvmul0or  30612  ipasslem5  30797  ipasslem11  30802  hvmul0or  30987  his6  31061  hhssnv  31226  ocsh  31245  ocin  31258  shsidmi  31346  chnlen0  31406  h1de2bi  31516  h1de2ctlem  31517  h1de2ci  31518  spansni  31519  3oalem1  31624  nmcexi  31988  atcveq0  32310  chcv1  32317  cdjreui  32394  cdj3lem2b  32399  xrge0tsmsd  33028  1fldgenq  33274  ccfldextdgrr  33646  ordtrest2NEWlem  33891  ordtrest2NEW  33892  xrge0iifcnv  33902  esumc  34020  esumpcvgval  34047  ballotlemfc0  34463  ballotlemfcc  34464  gblacfnacd  35077  subfacp1lem4  35158  subfacp1lem5  35159  erdszelem8  35173  sconnpi1  35214  cvmsss2  35249  cvmlift2lem12  35289  satfv0  35333  satfv0fun  35346  satf00  35349  sat1el2xp  35354  fmla0xp  35358  fmlasucdisj  35374  satffunlem1lem1  35377  satffunlem2lem1  35379  dmopab3rexdif  35380  msubco  35506  msubvrs  35535  ellcsrspsn  35616  sinccvglem  35647  untsucf  35685  nnuni  35702  dfrdg2  35771  colineardim1  36037  btwnconn1lem14  36076  segleantisym  36091  colinbtwnle  36094  outsidele  36108  lineunray  36123  linethru  36129  elicc3  36293  opnregcld  36306  cldregopn  36307  fnejoin2  36345  bj-isrvec  37270  dissneqlem  37316  icorempo  37327  relowlssretop  37339  relowlpssretop  37340  rdgssun  37354  finxpsuclem  37373  lindsenlbs  37597  ptrecube  37602  poimirlem6  37608  poimirlem7  37609  poimirlem16  37618  poimirlem17  37619  poimirlem19  37621  poimirlem20  37622  poimirlem21  37623  poimirlem22  37624  poimirlem23  37625  poimirlem24  37626  poimirlem25  37627  poimirlem26  37628  poimirlem27  37629  poimirlem29  37631  poimirlem30  37632  poimirlem31  37633  poimirlem32  37634  itg2addnclem3  37655  ftc1anclem6  37680  dvasin  37686  unirep  37696  sdclem2  37724  ssbnd  37770  prdsbnd  37775  cntotbnd  37778  heibor1lem  37791  rrnequiv  37817  ismndo2  37856  grpoeqdivid  37863  isdrngo3  37941  crngohomfo  37988  0idl  38007  1idl  38008  divrngidl  38010  smprngopr  38034  prnc  38049  ispridlc  38052  riotaclbgBAD  38935  lshpdisj  38968  lsateln0  38976  lsatcveq0  39013  opnlen0  39169  cmtbr4N  39236  cvrnbtwn2  39256  cvrnbtwn4  39260  atcvreq0  39295  cvlatexch1  39317  exatleN  39386  atlelt  39420  ps-2  39460  llnn0  39498  lplnn0N  39529  islpln2a  39530  lvoln0N  39573  islvol2aN  39574  4at  39595  dalemcea  39642  dalem3  39646  pmapglb2N  39753  pmapglb2xN  39754  cdlema1N  39773  cdlemb  39776  paddasslem17  39818  llnexchb2lem  39850  llnexchb2  39851  lhpat3  40028  ltrnid  40117  trlne  40167  cdlemc4  40176  cdleme11h  40248  cdlemednuN  40282  cdlemg1a  40552  tendoeq2  40756  tendoid0  40807  dva1dim  40967  dib1dim  41147  dihlatat  41319  dochkrshp4  41371  dochkr1  41460  lclkrlem2e  41493  lcfrlem16  41540  lcfrlem28  41552  mapd0  41647  hdmap14lem13  41862  eqresfnbd  42208  f1o2d2  42209  expeq1d  42300  expeqidd  42301  dvdsexpnn0  42310  reladdrsub  42361  sn-remul0ord  42384  sn-negex12  42393  sn-mullid  42412  sn-mul02  42428  nn0addcom  42438  nn0mulcom  42442  zmulcomlem  42443  mulgt0con1d  42446  mulgt0con2d  42447  sn-sup2  42467  frlmsnic  42516  evlselvlem  42562  prjspner1  42602  elrfi  42670  mrefg2  42683  eldiophb  42733  eldioph2b  42739  diophin  42748  diophun  42749  rexzrexnn0  42780  eldioph4b  42787  diophren  42789  rencldnfilem  42796  pellexlem6  42810  jm2.19  42969  rmydioph  42990  expdiophlem1  42997  expdioph  42999  lnr2i  43092  lpirlnr  43093  hbtlem2  43100  hbtlem4  43102  hbtlem6  43105  dgrsub2  43111  dgraa0p  43125  rngunsnply  43145  nlimsuc  43417  dfsucon  43499  radcnvrat  44290  pm14.24  44408  addrcom  44451  modelaxreplem1  44955  ormklocald  46859  natlocalincr  46861  afveu  47141  dfafn5b  47149  rlimdmafv  47165  afv2eu  47226  rlimdmafv2  47246  el1fzopredsuc  47313  minusmod5ne  47337  modmknepk  47350  elsetpreimafvssdm  47374  imasetpreimafvbijlemfo  47393  sprvalpw  47468  prprvalpw  47503  reupr  47510  fmtnofac2lem  47556  proththdlem  47601  perfectALTVlem2  47710  perfectALTV  47711  gbowpos  47747  gbowgt5  47750  gboge9  47752  nnsum4primesodd  47784  nnsum4primesoddALTV  47785  uhgrimedgi  47878  isuspgrim0  47882  isuspgrimlem  47883  upgrimpths  47897  clnbgrgrim  47922  grimedg  47923  grtrissvtx  47932  stgredgiun  47946  stgrvtx0  47950  isubgr3stgrlem7  47960  grlimgrtrilem2  47990  gpgiedgdmellem  48034  gpgvtxel2  48036  gpgvtx0  48041  gpgvtx1  48042  gpgusgralem  48044  gpgedgvtx0  48049  gpgedgvtx1  48050  gpgedg2ov  48054  gpgedg2iv  48055  gpgnbgrvtx0  48062  gpgnbgrvtx1  48063  pgnbgreunbgr  48113  ringcinvALTV  48298  lincellss  48415  lindsrng01  48457  suppdm  48499  nnpw2pb  48576  0aryfvalel  48623  0aryfvalelfv  48624  itsclc0xyqsolr  48758  infsubc  49049  infsubc2  49050