Theorem syl5ibrcom 246

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  biimprcd  249  elsn2g  4668  preq1b  4849  elpreqprb  4870  reusv3  5405  alxfr  5407  reuhypd  5419  opth1  5477  euotd  5515  otiunsndisj  5522  tz7.2  5662  frsn  5765  dmopab2rex  5920  elsnxp  6297  reuop  6299  dfpo2  6302  ordtri1  6404  ordtri3  6407  fvmptdv2  7022  fveqressseq  7088  foco2  7118  fsn  7144  fnsnb  7175  fmptsng  7177  fmptsnd  7178  fconst2g  7215  fnprb  7220  fntpb  7221  funfvima  7242  soisoi  7335  isores3  7342  eqfunresadj  7367  riotaeqimp  7402  eusvobj2  7411  ovmpodv2  7579  f1opw2  7676  sorpssun  7736  sorpssin  7737  oneqmin  7804  nlimsucg  7847  onzsl  7851  tfinds  7865  funcnvuni  7940  mptcnfimad  7991  opiota  8064  mposn  8108  frpoins3xpg  8145  frpoins3xp3g  8146  poxp2  8148  xpord2pred  8150  sexp2  8151  poxp3  8155  xpord3pred  8157  sexp3  8158  xpord3inddlem  8159  suppssov1  8203  suppssov2  8204  suppssfv  8208  brtpos  8241  frrlem12  8303  frrlem13  8304  wfrlem10OLD  8339  wfrlem14OLD  8343  wfrlem15OLD  8344  seqomlem1  8471  seqomlem2  8472  omordi  8587  omord  8589  omwordi  8592  oeeui  8623  nnmordi  8652  nnmord  8653  nnmwordi  8656  nnawordex  8658  nnaordex  8659  nneob  8677  omsmolem  8678  eldifsucnn  8685  qsss  8797  eroveu  8831  mapsncnv  8912  ralxpmap  8915  elixpsn  8956  ixpsnf1o  8957  boxcutc  8960  pw2f1olem  9101  2pwne  9158  mapxpen  9168  mapunen  9171  php  9235  phpOLD  9247  onomeneq  9253  unxpdomlem2  9276  en1eqsnbi  9301  isfiniteg  9329  fofinf1o  9353  f1opwfi  9382  elfiun  9455  oieu  9564  brwdom2  9598  wdomtr  9600  ixpiunwdom  9615  en3lplem1  9637  suc11reg  9644  inf3lemd  9652  cantnfvalf  9690  cantnflt  9697  cantnfp1lem3  9705  cantnflem2  9715  ttrcltr  9741  rnttrcl  9747  ttrclselem1  9750  r1tr  9801  updjud  9959  dfac8alem  10054  wdomnumr  10089  isinfcard  10117  aceq3lem  10145  dfac5lem4  10151  dfac5  10153  dfac2b  10155  coftr  10298  fin23lem28  10365  fin23lem29  10366  fin1a2lem11  10435  fin1a2lem12  10436  fin1a2lem13  10437  hsmexlem9  10450  axdclem  10544  pwcfsdom  10608  gchdomtri  10654  fpwwe2  10668  gchpwdom  10695  gchhar  10704  addnidpi  10926  nqereu  10954  genpv  11024  genpdm  11027  distrlem5pr  11052  mulrid  11244  ltne  11343  mul02  11424  cnegex  11427  mul0or  11886  negfi  12196  sup2  12203  supaddc  12214  supadd  12215  supmul1  12216  supmul  12219  creur  12239  creui  12240  cju  12241  nnsub  12289  un0addcl  12538  un0mulcl  12539  nn0sub  12555  elz2  12609  zaddcl  12635  suprzcl2  12955  qmulz  12968  qre  12970  qnegcl  12983  elpqb  12993  xrmax1  13189  xrmin2  13192  max1ALT  13200  xlesubadd  13277  xmulass  13301  xlemul1a  13302  xrsupexmnf  13319  xrinfmexpnf  13320  xrub  13326  iccid  13404  fzsn  13578  fzsuc2  13594  fz1sbc  13612  elfzp12  13615  modmuladd  13914  seqid3  14047  bcval5  14313  bcpasc  14316  hashbnd  14331  hashnnn0genn0  14338  hashprg  14390  hashfzo  14424  wrdl1s1  14600  ccats1alpha  14605  cats1un  14707  shftlem  15051  replim  15099  absmod0  15286  absz  15294  rlimdm  15531  summolem2  15698  summo  15699  zsum  15700  fsum  15702  fsummulc2  15766  fsumconst  15772  fsum00  15780  incexclem  15818  isumsplit  15822  infcvgaux1i  15839  prodmolem2  15915  prodmo  15916  zprod  15917  fprod  15921  prodsn  15942  prodsnf  15944  fprodconst  15958  ruclem2  16212  fzo0dvdseq  16303  bitsf1ocnv  16422  sadcaddlem  16435  smueqlem  16468  gcdabs1  16507  bezoutlem1  16518  bezoutlem3  16520  bezoutlem4  16521  dvdsgcd  16523  dvdsmulgcd  16534  lcmgcdeq  16586  lcmf  16607  lcmfunsnlem1  16611  lcmfunsnlem2lem2  16613  isprm2lem  16655  dvdsprime  16661  isprm5  16681  coprm  16685  prmdvdsexpr  16691  rpexp  16697  phibndlem  16742  dfphi2  16746  hashgcdlem  16760  odzdvds  16767  nnoddn2prm  16783  pythagtriplem1  16788  iserodd  16807  pceulem  16817  pcqmul  16825  pcqcl  16828  pcxnn0cl  16832  pcxcl  16833  pcneg  16846  pcabs  16847  pcgcd1  16849  pcz  16853  pcprmpw2  16854  pcprmpw  16855  dvdsprmpweqle  16858  difsqpwdvds  16859  pcaddlem  16860  pcadd  16861  pcmpt  16864  pockthg  16878  prmreclem5  16892  4sqlem4  16924  mul4sq  16926  vdwapun  16946  vdwlem2  16954  vdwlem6  16958  vdwlem8  16960  vdwlem13  16965  0ram  16992  ram0  16994  ramcl  17001  cshwsiun  17072  wunress  17234  wunressOLD  17235  firest  17417  isssc  17806  pospo  18340  latnlej  18451  gsumval2a  18648  xpsmnd0  18738  mnd1id  18740  0subm  18777  mulgnn0p1  19048  mulgnn0ass  19073  cyccom  19166  gicsubgen  19242  symg1bas  19357  snsymgefmndeq  19361  psgnunilem1  19460  psgnunilem2  19462  mndodcongi  19510  oddvdsnn0  19511  odnncl  19512  oddvds  19514  odeq  19517  odeq1  19527  pgpfi2  19573  sylow2a  19586  sylow2blem3  19589  sylow3lem6  19599  lsmelvalm  19618  lsmsubm  19620  lsmsubg  19621  lsmmod  19642  lsmdisj2  19649  efgmnvl  19681  efgtlen  19693  efgs1b  19703  efgrelexlemb  19717  efgredeu  19719  efgcpbllemb  19722  frgpuptinv  19738  frgpup3lem  19744  qusabl  19832  frgpnabllem1  19840  cyggeninv  19850  cyggenod  19851  gsumval3eu  19871  dprdssv  19985  dprdfeq0  19991  dprdsubg  19993  dprddisj2  20008  ablfacrp  20035  pgpfac1lem3  20046  pgpfaclem2  20051  xpsring1d  20281  dvreq1  20362  irredn1  20377  nzrunit  20473  ringcinv  20616  drngmul0or  20665  isabvd  20712  abvdom  20730  issrngd  20753  lmodfopnelem2  20794  lss1d  20859  lspsneq0  20908  lbspss  20979  lsmcl  20980  lvecvs0or  21008  lspindpi  21032  lidl1el  21134  lpiss  21236  lidldvgen  21241  rrgeq0  21254  domneq0  21261  qsssubdrg  21376  zringlpirlem1  21405  pzriprnglem6  21429  pzriprnglem12  21435  znfld  21511  znunit  21514  znrrg  21516  cygznlem3  21520  frgpcyg  21524  psgnghm  21529  ipeq0  21587  cssincl  21637  lsmcss  21641  obselocv  21679  dsmmacl  21692  dsmmlss  21695  mplsubrglem  21966  mplmonmul  21996  mplcoe5lem  21999  mhpsclcl  22094  mhpvarcl  22095  psdmul  22113  coe1tmmul2  22220  coe1tmmul  22221  pf1ind  22299  mat1dimelbas  22417  mdetralt  22554  mdetunilem2  22559  mdetunilem7  22564  mdetunilem9  22566  maducoeval2  22586  chpscmat  22788  chfacfscmulgsum  22806  chfacfpmmulgsum  22810  istopon  22858  eltg3  22909  tgidm  22927  clsval2  22998  opncldf1  23032  restbas  23106  tgrest  23107  restcld  23120  restcldr  23122  restcls  23129  restntr  23130  ordtbas2  23139  ordtbas  23140  ordtrest2lem  23151  ordtrest2  23152  pnfnei  23168  mnfnei  23169  tgcn  23200  cnconst  23232  cnindis  23240  lmss  23246  ordtt1  23327  discmp  23346  1stcrest  23401  2ndcdisj  23404  cldllycmp  23443  txbas  23515  ptpjpre1  23519  ptuni2  23524  ptbasin  23525  ptbasfi  23529  ptopn2  23532  txbasval  23554  ptpjopn  23560  ptclsg  23563  dfac14lem  23565  xkoccn  23567  ptcnp  23570  upxp  23571  ptrescn  23587  txkgen  23600  xkoptsub  23602  xkopt  23603  xkoco1cn  23605  xkoco2cn  23606  xkococn  23608  xkoinjcn  23635  ordthmeolem  23749  ptuncnv  23755  nrmhaus  23774  fbssint  23786  fbfinnfr  23789  fbasrn  23832  isufil2  23856  filufint  23868  rnelfm  23901  fmfnfmlem2  23903  fmfnfmlem3  23904  fmfnfmlem4  23905  fmfnfm  23906  flimtopon  23918  flimclslem  23932  fclstopon  23960  fclscf  23973  flimfnfcls  23976  alexsublem  23992  alexsubALTlem3  23997  alexsubALTlem4  23998  ptcmplem2  24001  tmdgsum2  24044  symgtgp  24054  cldsubg  24059  qustgplem  24069  tgptsmscld  24099  tsmsxplem1  24101  imasdsf1olem  24323  blssps  24374  blss  24375  stdbdxmet  24468  methaus  24473  metrest  24477  nrginvrcn  24653  nmoeq0  24697  blssioo  24755  xrtgioo  24766  xrsxmet  24769  reconnlem1  24786  reconnlem2  24787  xrge0tsms  24794  elcncf1di  24859  iccpnfcnv  24913  evth  24929  lebnumlem1  24931  lebnumlem2  24932  lebnumlem3  24933  nmoleub3  25090  minveclem3b  25400  ivthlem2  25425  ivthlem3  25426  elovolm  25448  ovolmge0  25450  ovoliun  25478  ovolicc2lem3  25492  ovolicc2  25495  voliunlem3  25525  dyaddisj  25569  dyadmax  25571  opnmblALT  25576  ismbfd  25612  ismbf2d  25613  mbfimaopnlem  25628  mbfimaopn2  25630  i1fmullem  25667  i1fres  25679  itg1climres  25688  mbfi1fseqlem4  25692  itg2lcl  25701  itgsplitioo  25811  ellimc2  25850  rolle  25966  dvlip  25970  dvge0  25983  dvne0  25988  lhop1lem  25990  tdeglem4  26039  tdeglem4OLD  26040  degltlem1  26052  deg1nn0clb  26070  deg1lt0  26071  dvdsq1p  26142  ply1rem  26145  fta1g  26149  elply2  26175  plyf  26177  ne0p  26186  plyeq0lem  26189  plypf1  26191  0dgrb  26225  coe1termlem  26237  dgrcolem2  26254  plymul0or  26260  plyrem  26285  fta1  26288  quotcan  26289  aalioulem3  26314  eff1olem  26527  lognegb  26569  eflogeq  26581  argregt0  26589  argrege0  26590  tanarg  26598  cxpexp  26647  cxpeq0  26657  mulcxp  26664  cxpeq  26737  atans2  26908  scvxcvx  26963  dmgmaddn0  27000  isppw2  27092  vmappw  27093  vmacl  27095  efvmacl  27097  isnsqf  27112  mumullem2  27157  sqff1o  27159  dvdsppwf1o  27163  ppiublem1  27180  vmalelog  27183  chtublem  27189  fsumvma  27191  perfectlem2  27208  perfect  27209  bposlem1  27262  lgsmod  27301  lgsne0  27313  lgsdirnn0  27322  lgsqr  27329  lgsdchr  27333  gausslemma2dlem1a  27343  gausslemma2dlem6  27350  lgseisenlem2  27354  lgsquadlem1  27358  lgsquadlem2  27359  2lgslem1b  27370  2sqlem2  27396  mul2sq  27397  2sqlem7  27402  dchrisum0fno1  27489  pntrsumbnd2  27545  ostthlem1  27605  ostth2lem2  27612  ostth3  27616  ostth  27617  nolesgn2ores  27651  nogesgn1ores  27653  nolt02o  27674  nogt01o  27675  nosupbnd2  27695  noinfbnd2lem1  27709  noetasuplem4  27715  noetainflem4  27719  maxs1  27744  mins2  27747  sltne  27749  ssltsn  27771  cuteq1  27812  madef  27829  sltlpss  27879  lrrecfr  27906  addsval  27925  addsproplem2  27933  addsuniflem  27964  negsid  27999  negsunif  28013  mulsproplem5  28070  mulsproplem6  28071  mulsproplem7  28072  mulsproplem8  28073  mulsproplem9  28074  slemuld  28088  ssltmul1  28097  ssltmul2  28098  sltmul2  28121  muls0ord  28135  precsexlem8  28162  precsexlem9  28163  precsexlem11  28165  elons2  28201  n0subs  28275  znegscl  28289  elzn0s  28291  recut  28296  0reno  28297  remulscllem1  28300  colinearalg  28793  axpasch  28824  axlowdimlem16  28840  axlowdimlem17  28841  axlowdim  28844  axcontlem2  28848  axcontlem4  28850  axcontlem7  28853  lpvtx  28953  edglnl  29028  numedglnl  29029  usgredgop  29055  usgrexmplef  29144  uhgrspansubgrlem  29175  uhgrspan1  29188  nbusgredgeu0  29253  nb3grprlem2  29266  cusgrsize2inds  29339  vtxd0nedgb  29374  rusgrpropnb  29469  upgrwlkvtxedg  29531  wlkp1lem1  29559  wlkp1lem6  29564  wlkp1lem8  29566  usgr2wlkneq  29642  crctcshwlk  29705  crctcsh  29707  iswwlksnon  29736  wlkiswwlks1  29750  wwlksnextbi  29777  wwlksnextproplem2  29793  wspthsnonn0vne  29800  clwlkclwwlklem2  29882  clwwisshclwws  29897  erclwwlktr  29904  clwwlkel  29928  clwwlkext2edg  29938  erclwwlkntr  29953  clwlknf1oclwwlknlem2  29964  clwlknf1oclwwlknlem3  29965  clwlknf1oclwwlkn  29966  clwwlknonccat  29978  0wlkons1  30003  3wlkdlem6  30047  eupth2eucrct  30099  frgrwopreglem2  30195  2clwwlk2clwwlk  30232  wlkl0  30249  nvmul0or  30532  ipasslem5  30717  ipasslem11  30722  hvmul0or  30907  his6  30981  hhssnv  31146  ocsh  31165  ocin  31178  shsidmi  31266  chnlen0  31326  h1de2bi  31436  h1de2ctlem  31437  h1de2ci  31438  spansni  31439  3oalem1  31544  nmcexi  31908  atcveq0  32230  chcv1  32237  cdjreui  32314  cdj3lem2b  32319  xrge0tsmsd  32861  1fldgenq  33108  ccfldextdgrr  33491  ordtrest2NEWlem  33654  ordtrest2NEW  33655  xrge0iifcnv  33665  esumc  33801  esumpcvgval  33828  ballotlemfc0  34243  ballotlemfcc  34244  subfacp1lem4  34924  subfacp1lem5  34925  erdszelem8  34939  sconnpi1  34980  cvmsss2  35015  cvmlift2lem12  35055  satfv0  35099  satfv0fun  35112  satf00  35115  sat1el2xp  35120  fmla0xp  35124  fmlasucdisj  35140  satffunlem1lem1  35143  satffunlem2lem1  35145  dmopab3rexdif  35146  msubco  35272  msubvrs  35301  sinccvglem  35407  untsucf  35435  nnuni  35452  dfrdg2  35522  colineardim1  35788  btwnconn1lem14  35827  segleantisym  35842  colinbtwnle  35845  outsidele  35859  lineunray  35874  linethru  35880  elicc3  35932  opnregcld  35945  cldregopn  35946  fnejoin2  35984  bj-isrvec  36904  dissneqlem  36950  icorempo  36961  relowlssretop  36973  relowlpssretop  36974  rdgssun  36988  finxpsuclem  37007  lindsenlbs  37219  ptrecube  37224  poimirlem6  37230  poimirlem7  37231  poimirlem16  37240  poimirlem17  37241  poimirlem19  37243  poimirlem20  37244  poimirlem21  37245  poimirlem22  37246  poimirlem23  37247  poimirlem24  37248  poimirlem25  37249  poimirlem26  37250  poimirlem27  37251  poimirlem29  37253  poimirlem30  37254  poimirlem31  37255  poimirlem32  37256  itg2addnclem3  37277  ftc1anclem6  37302  dvasin  37308  unirep  37318  sdclem2  37346  ssbnd  37392  prdsbnd  37397  cntotbnd  37400  heibor1lem  37413  rrnequiv  37439  ismndo2  37478  grpoeqdivid  37485  isdrngo3  37563  crngohomfo  37610  0idl  37629  1idl  37630  divrngidl  37632  smprngopr  37656  prnc  37671  ispridlc  37674  riotaclbgBAD  38556  lshpdisj  38589  lsateln0  38597  lsatcveq0  38634  opnlen0  38790  cmtbr4N  38857  cvrnbtwn2  38877  cvrnbtwn4  38881  atcvreq0  38916  cvlatexch1  38938  exatleN  39007  atlelt  39041  ps-2  39081  llnn0  39119  lplnn0N  39150  islpln2a  39151  lvoln0N  39194  islvol2aN  39195  4at  39216  dalemcea  39263  dalem3  39267  pmapglb2N  39374  pmapglb2xN  39375  cdlema1N  39394  cdlemb  39397  paddasslem17  39439  llnexchb2lem  39471  llnexchb2  39472  lhpat3  39649  ltrnid  39738  trlne  39788  cdlemc4  39797  cdleme11h  39869  cdlemednuN  39903  cdlemg1a  40173  tendoeq2  40377  tendoid0  40428  dva1dim  40588  dib1dim  40768  dihlatat  40940  dochkrshp4  40992  dochkr1  41081  lclkrlem2e  41114  lcfrlem16  41161  lcfrlem28  41173  mapd0  41268  hdmap14lem13  41483  fnsnbt  41854  eqresfnbd  41856  f1o2d2  41857  frlmsnic  41908  evlselvlem  41954  dvdsexpnn0  42036  reladdrsub  42075  sn-negex12  42106  sn-mullid  42125  sn-mul02  42130  nn0addcom  42140  nn0mulcom  42144  zmulcomlem  42145  mulgt0con1d  42148  mulgt0con2d  42149  sn-sup2  42159  prjspner1  42185  elrfi  42256  mrefg2  42269  eldiophb  42319  eldioph2b  42325  diophin  42334  diophun  42335  rexzrexnn0  42366  eldioph4b  42373  diophren  42375  rencldnfilem  42382  pellexlem6  42396  jm2.19  42556  rmydioph  42577  expdiophlem1  42584  expdioph  42586  lnr2i  42682  lpirlnr  42683  hbtlem2  42690  hbtlem4  42692  hbtlem6  42695  dgrsub2  42701  dgraa0p  42715  rngunsnply  42739  nlimsuc  43013  dfsucon  43095  radcnvrat  43893  pm14.24  44011  addrcom  44054  natlocalincr  46400  afveu  46671  dfafn5b  46679  rlimdmafv  46695  afv2eu  46756  rlimdmafv2  46776  el1fzopredsuc  46843  elsetpreimafvssdm  46863  imasetpreimafvbijlemfo  46882  sprvalpw  46957  prprvalpw  46992  reupr  46999  fmtnofac2lem  47045  proththdlem  47090  perfectALTVlem2  47199  perfectALTV  47200  gbowpos  47236  gbowgt5  47239  gboge9  47241  nnsum4primesodd  47273  nnsum4primesoddALTV  47274  isuspgrim0  47356  isuspgrimlem  47358  ringcinvALTV  47558  lincellss  47680  lindsrng01  47722  suppdm  47764  nnpw2pb  47846  0aryfvalel  47893  0aryfvalelfv  47894  itsclc0xyqsolr  48028