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  4513  elsn2g  4640  preq1b  4822  elpreqprb  4844  reusv3  5375  alxfr  5377  reuhypd  5389  axpr  5397  opth1  5450  euotd  5488  otiunsndisj  5495  tz7.2  5637  frsn  5742  dmopab2rex  5897  elsnxp  6280  reuop  6282  dfpo2  6285  ordtri1  6385  ordtri3  6388  fvmptdv2  7003  fveqressseq  7068  foco2  7098  fsn  7124  fnsnbg  7155  fnsnbOLD  7157  fmptsng  7159  fmptsnd  7160  fconst2g  7194  fnprb  7199  fntpb  7200  funfvima  7221  soisoi  7320  isores3  7327  eqfunresadj  7352  riotaeqimp  7386  eusvobj2  7395  ovmpodv2  7563  f1opw2  7660  sorpssun  7722  sorpssin  7723  oneqmin  7792  nlimsucg  7835  onzsl  7839  tfinds  7853  funcnvuni  7926  mptcnfimad  7983  opiota  8056  mposn  8100  frpoins3xpg  8137  frpoins3xp3g  8138  poxp2  8140  xpord2pred  8142  sexp2  8143  poxp3  8147  xpord3pred  8149  sexp3  8150  xpord3inddlem  8151  suppssov1  8194  suppssov2  8195  suppssfv  8199  brtpos  8232  frrlem12  8294  frrlem13  8295  wfrlem10OLD  8330  wfrlem14OLD  8334  wfrlem15OLD  8335  seqomlem1  8462  seqomlem2  8463  omordi  8576  omord  8578  omwordi  8581  oeeui  8612  nnmordi  8641  nnmord  8642  nnmwordi  8645  nnawordex  8647  nnaordex  8648  nneob  8666  omsmolem  8667  eldifsucnn  8674  qsss  8790  eroveu  8824  mapsncnv  8905  ralxpmap  8908  elixpsn  8949  ixpsnf1o  8950  boxcutc  8953  pw2f1olem  9088  2pwne  9145  mapxpen  9155  mapunen  9158  php  9219  phpOLD  9229  onomeneq  9235  unxpdomlem2  9257  en1eqsnbi  9280  isfiniteg  9307  fofinf1o  9342  f1opwfi  9366  elfiun  9440  oieu  9551  brwdom2  9585  wdomtr  9587  ixpiunwdom  9602  en3lplem1  9624  suc11reg  9631  inf3lemd  9639  cantnfvalf  9677  cantnflt  9684  cantnfp1lem3  9692  cantnflem2  9702  ttrcltr  9728  rnttrcl  9734  ttrclselem1  9737  r1tr  9788  updjud  9946  dfac8alem  10041  wdomnumr  10076  isinfcard  10104  aceq3lem  10132  dfac5lem4  10138  dfac5lem4OLD  10140  dfac5  10141  dfac2b  10143  coftr  10285  fin23lem28  10352  fin23lem29  10353  fin1a2lem11  10422  fin1a2lem12  10423  fin1a2lem13  10424  hsmexlem9  10437  axdclem  10531  pwcfsdom  10595  gchdomtri  10641  fpwwe2  10655  gchpwdom  10682  gchhar  10691  addnidpi  10913  nqereu  10941  genpv  11011  genpdm  11014  distrlem5pr  11039  mulrid  11231  ltne  11330  mul02  11411  cnegex  11414  mul0or  11875  negfi  12189  sup2  12196  supaddc  12207  supadd  12208  supmul1  12209  supmul  12212  creur  12232  creui  12233  cju  12234  nnsub  12282  un0addcl  12532  un0mulcl  12533  nn0sub  12549  elz2  12604  zaddcl  12630  suprzcl2  12952  qmulz  12965  qre  12967  qnegcl  12980  elpqb  12990  xrmax1  13189  xrmin2  13192  max1ALT  13200  xlesubadd  13277  xmulass  13301  xlemul1a  13302  xrsupexmnf  13319  xrinfmexpnf  13320  xrub  13326  iccid  13405  fzsn  13581  fzsuc2  13597  fz1sbc  13615  elfzp12  13618  modmuladd  13929  seqid3  14062  bcval5  14334  bcpasc  14337  hashbnd  14352  hashnnn0genn0  14359  hashprg  14411  hashfzo  14445  tpfo  14516  wrdl1s1  14630  ccats1alpha  14635  cats1un  14737  s7f1o  14983  shftlem  15085  replim  15133  absmod0  15320  absz  15328  rlimdm  15565  summolem2  15730  summo  15731  zsum  15732  fsum  15734  fsummulc2  15798  fsumconst  15804  fsum00  15812  incexclem  15850  isumsplit  15854  infcvgaux1i  15871  prodmolem2  15949  prodmo  15950  zprod  15951  fprod  15955  prodsn  15976  prodsnf  15978  fprodconst  15992  ruclem2  16248  fzo0dvdseq  16340  bitsf1ocnv  16461  sadcaddlem  16474  smueqlem  16507  gcdabs1  16546  bezoutlem1  16556  bezoutlem3  16558  bezoutlem4  16559  dvdsgcd  16561  dvdsmulgcd  16573  lcmgcdeq  16629  lcmf  16650  lcmfunsnlem1  16654  lcmfunsnlem2lem2  16656  isprm2lem  16698  dvdsprime  16704  isprm5  16724  coprm  16728  prmdvdsexpr  16734  rpexp  16739  phibndlem  16787  dfphi2  16791  hashgcdlem  16805  odzdvds  16813  nnoddn2prm  16829  pythagtriplem1  16834  iserodd  16853  pceulem  16863  pcqmul  16871  pcqcl  16874  pcxnn0cl  16878  pcxcl  16879  pcneg  16892  pcabs  16893  pcgcd1  16895  pcz  16899  pcprmpw2  16900  pcprmpw  16901  dvdsprmpweqle  16904  difsqpwdvds  16905  pcaddlem  16906  pcadd  16907  pcmpt  16910  pockthg  16924  prmreclem5  16938  4sqlem4  16970  mul4sq  16972  vdwapun  16992  vdwlem2  17000  vdwlem6  17004  vdwlem8  17006  vdwlem13  17011  0ram  17038  ram0  17040  ramcl  17047  cshwsiun  17117  wunress  17268  firest  17444  isssc  17831  pospo  18353  latnlej  18464  gsumval2a  18661  xpsmnd0  18754  mnd1id  18756  0subm  18793  mulgnn0p1  19066  mulgnn0ass  19091  cyccom  19184  gicsubgen  19260  symg1bas  19370  snsymgefmndeq  19374  psgnunilem1  19472  psgnunilem2  19474  mndodcongi  19522  oddvdsnn0  19523  odnncl  19524  oddvds  19526  odeq  19529  odeq1  19539  pgpfi2  19585  sylow2a  19598  sylow2blem3  19601  sylow3lem6  19611  lsmelvalm  19630  lsmsubm  19632  lsmsubg  19633  lsmmod  19654  lsmdisj2  19661  efgmnvl  19693  efgtlen  19705  efgs1b  19715  efgrelexlemb  19729  efgredeu  19731  efgcpbllemb  19734  frgpuptinv  19750  frgpup3lem  19756  qusabl  19844  frgpnabllem1  19852  cyggeninv  19862  cyggenod  19863  gsumval3eu  19883  dprdssv  19997  dprdfeq0  20003  dprdsubg  20005  dprddisj2  20020  ablfacrp  20047  pgpfac1lem3  20058  pgpfaclem2  20063  xpsring1d  20291  dvreq1  20369  irredn1  20384  nzrunit  20482  ringcinv  20629  rrgeq0  20658  domneq0  20666  drngmul0orOLD  20719  isabvd  20770  abvdom  20788  issrngd  20813  lmodfopnelem2  20854  lss1d  20918  lspsneq0  20967  lbspss  21038  lsmcl  21039  lvecvs0or  21067  lspindpi  21091  lidl1el  21185  lpiss  21288  lidldvgen  21293  qsssubdrg  21392  zringlpirlem1  21421  pzriprnglem6  21445  pzriprnglem12  21451  znfld  21519  znunit  21522  znrrg  21524  cygznlem3  21528  frgpcyg  21532  psgnghm  21538  ipeq0  21596  cssincl  21646  lsmcss  21650  obselocv  21686  dsmmacl  21699  dsmmlss  21702  mplsubrglem  21962  mplmonmul  21992  mplcoe5lem  21995  mhpsclcl  22083  mhpvarcl  22084  psdmul  22102  coe1tmmul2  22211  coe1tmmul  22212  pf1ind  22291  mat1dimelbas  22407  mdetralt  22544  mdetunilem2  22549  mdetunilem7  22554  mdetunilem9  22556  maducoeval2  22576  chpscmat  22778  chfacfscmulgsum  22796  chfacfpmmulgsum  22800  istopon  22848  eltg3  22898  tgidm  22916  clsval2  22986  opncldf1  23020  restbas  23094  tgrest  23095  restcld  23108  restcldr  23110  restcls  23117  restntr  23118  ordtbas2  23127  ordtbas  23128  ordtrest2lem  23139  ordtrest2  23140  pnfnei  23156  mnfnei  23157  tgcn  23188  cnconst  23220  cnindis  23228  lmss  23234  ordtt1  23315  discmp  23334  1stcrest  23389  2ndcdisj  23392  cldllycmp  23431  txbas  23503  ptpjpre1  23507  ptuni2  23512  ptbasin  23513  ptbasfi  23517  ptopn2  23520  txbasval  23542  ptpjopn  23548  ptclsg  23551  dfac14lem  23553  xkoccn  23555  ptcnp  23558  upxp  23559  ptrescn  23575  txkgen  23588  xkoptsub  23590  xkopt  23591  xkoco1cn  23593  xkoco2cn  23594  xkococn  23596  xkoinjcn  23623  ordthmeolem  23737  ptuncnv  23743  nrmhaus  23762  fbssint  23774  fbfinnfr  23777  fbasrn  23820  isufil2  23844  filufint  23856  rnelfm  23889  fmfnfmlem2  23891  fmfnfmlem3  23892  fmfnfmlem4  23893  fmfnfm  23894  flimtopon  23906  flimclslem  23920  fclstopon  23948  fclscf  23961  flimfnfcls  23964  alexsublem  23980  alexsubALTlem3  23985  alexsubALTlem4  23986  ptcmplem2  23989  tmdgsum2  24032  symgtgp  24042  cldsubg  24047  qustgplem  24057  tgptsmscld  24087  tsmsxplem1  24089  imasdsf1olem  24310  blssps  24361  blss  24362  stdbdxmet  24452  methaus  24457  metrest  24461  nrginvrcn  24629  nmoeq0  24673  blssioo  24732  xrtgioo  24744  xrsxmet  24747  reconnlem1  24764  reconnlem2  24765  xrge0tsms  24772  elcncf1di  24837  iccpnfcnv  24891  evth  24907  lebnumlem1  24909  lebnumlem2  24910  lebnumlem3  24911  nmoleub3  25068  minveclem3b  25378  ivthlem2  25403  ivthlem3  25404  elovolm  25426  ovolmge0  25428  ovoliun  25456  ovolicc2lem3  25470  ovolicc2  25473  voliunlem3  25503  dyaddisj  25547  dyadmax  25549  opnmblALT  25554  ismbfd  25590  ismbf2d  25591  mbfimaopnlem  25606  mbfimaopn2  25608  i1fmullem  25645  i1fres  25656  itg1climres  25665  mbfi1fseqlem4  25669  itg2lcl  25678  itgsplitioo  25789  ellimc2  25828  rolle  25944  dvlip  25948  dvge0  25961  dvne0  25966  lhop1lem  25968  tdeglem4  26015  degltlem1  26027  deg1nn0clb  26045  deg1lt0  26046  dvdsq1p  26118  ply1rem  26121  fta1g  26125  elply2  26151  plyf  26153  ne0p  26162  plyeq0lem  26165  plypf1  26167  0dgrb  26201  coe1termlem  26213  dgrcolem2  26230  plymul0or  26238  plyrem  26263  fta1  26266  quotcan  26267  aalioulem3  26292  eff1olem  26507  lognegb  26549  eflogeq  26561  argregt0  26569  argrege0  26570  tanarg  26578  cxpexp  26627  cxpeq0  26637  mulcxp  26644  cxpeq  26717  atans2  26891  scvxcvx  26946  dmgmaddn0  26983  isppw2  27075  vmappw  27076  vmacl  27078  efvmacl  27080  isnsqf  27095  mumullem2  27140  sqff1o  27142  dvdsppwf1o  27146  ppiublem1  27163  vmalelog  27166  chtublem  27172  fsumvma  27174  perfectlem2  27191  perfect  27192  bposlem1  27245  lgsmod  27284  lgsne0  27296  lgsdirnn0  27305  lgsqr  27312  lgsdchr  27316  gausslemma2dlem1a  27326  gausslemma2dlem6  27333  lgseisenlem2  27337  lgsquadlem1  27341  lgsquadlem2  27342  2lgslem1b  27353  2sqlem2  27379  mul2sq  27380  2sqlem7  27385  dchrisum0fno1  27472  pntrsumbnd2  27528  ostthlem1  27588  ostth2lem2  27595  ostth3  27599  ostth  27600  nolesgn2ores  27634  nogesgn1ores  27636  nolt02o  27657  nogt01o  27658  nosupbnd2  27678  noinfbnd2lem1  27692  noetasuplem4  27698  noetainflem4  27702  maxs1  27727  mins2  27730  sltne  27732  ssltsn  27754  cuteq1  27795  madef  27812  sltlpss  27862  lrrecfr  27893  addsval  27912  addsproplem2  27920  addsuniflem  27951  addsbdaylem  27966  negsid  27990  negsunif  28004  mulsproplem5  28063  mulsproplem6  28064  mulsproplem7  28065  mulsproplem8  28066  mulsproplem9  28067  slemuld  28081  ssltmul1  28090  ssltmul2  28091  sltmul2  28114  muls0ord  28128  precsexlem8  28155  precsexlem9  28156  precsexlem11  28158  elons2  28198  onaddscl  28203  onmulscl  28204  nnsge1  28263  n0subs  28277  dfnns2  28279  znegscl  28295  zaddscl  28297  zmulscld  28300  elzn0s  28301  eln0zs  28303  n0seo  28322  zseo  28323  zs12bday  28341  recut  28345  0reno  28346  remulscllem1  28349  colinearalg  28835  axpasch  28866  axlowdimlem16  28882  axlowdimlem17  28883  axlowdim  28886  axcontlem2  28890  axcontlem4  28892  axcontlem7  28895  lpvtx  28993  edglnl  29068  numedglnl  29069  usgredgop  29095  usgrexmplef  29184  uhgrspansubgrlem  29215  uhgrspan1  29228  nbusgredgeu0  29293  nb3grprlem2  29306  cusgrsize2inds  29379  vtxd0nedgb  29414  rusgrpropnb  29509  upgrwlkvtxedg  29571  wlkp1lem1  29599  wlkp1lem6  29604  wlkp1lem8  29606  usgr2wlkneq  29684  crctcshwlk  29750  crctcsh  29752  iswwlksnon  29781  wlkiswwlks1  29795  wwlksnextbi  29822  wwlksnextproplem2  29838  wspthsnonn0vne  29845  clwlkclwwlklem2  29927  clwwisshclwws  29942  erclwwlktr  29949  clwwlkel  29973  clwwlkext2edg  29983  erclwwlkntr  29998  clwlknf1oclwwlknlem2  30009  clwlknf1oclwwlknlem3  30010  clwlknf1oclwwlkn  30011  clwwlknonccat  30023  0wlkons1  30048  3wlkdlem6  30092  eupth2eucrct  30144  frgrwopreglem2  30240  2clwwlk2clwwlk  30277  wlkl0  30294  nvmul0or  30577  ipasslem5  30762  ipasslem11  30767  hvmul0or  30952  his6  31026  hhssnv  31191  ocsh  31210  ocin  31223  shsidmi  31311  chnlen0  31371  h1de2bi  31481  h1de2ctlem  31482  h1de2ci  31483  spansni  31484  3oalem1  31589  nmcexi  31953  atcveq0  32275  chcv1  32282  cdjreui  32359  cdj3lem2b  32364  xrge0tsmsd  33002  1fldgenq  33262  ccfldextdgrr  33659  ordtrest2NEWlem  33899  ordtrest2NEW  33900  xrge0iifcnv  33910  esumc  34028  esumpcvgval  34055  ballotlemfc0  34471  ballotlemfcc  34472  gblacfnacd  35076  subfacp1lem4  35151  subfacp1lem5  35152  erdszelem8  35166  sconnpi1  35207  cvmsss2  35242  cvmlift2lem12  35282  satfv0  35326  satfv0fun  35339  satf00  35342  sat1el2xp  35347  fmla0xp  35351  fmlasucdisj  35367  satffunlem1lem1  35370  satffunlem2lem1  35372  dmopab3rexdif  35373  msubco  35499  msubvrs  35528  ellcsrspsn  35609  sinccvglem  35640  untsucf  35673  nnuni  35690  dfrdg2  35759  colineardim1  36025  btwnconn1lem14  36064  segleantisym  36079  colinbtwnle  36082  outsidele  36096  lineunray  36111  linethru  36117  elicc3  36281  opnregcld  36294  cldregopn  36295  fnejoin2  36333  bj-isrvec  37258  dissneqlem  37304  icorempo  37315  relowlssretop  37327  relowlpssretop  37328  rdgssun  37342  finxpsuclem  37361  lindsenlbs  37585  ptrecube  37590  poimirlem6  37596  poimirlem7  37597  poimirlem16  37606  poimirlem17  37607  poimirlem19  37609  poimirlem20  37610  poimirlem21  37611  poimirlem22  37612  poimirlem23  37613  poimirlem24  37614  poimirlem25  37615  poimirlem26  37616  poimirlem27  37617  poimirlem29  37619  poimirlem30  37620  poimirlem31  37621  poimirlem32  37622  itg2addnclem3  37643  ftc1anclem6  37668  dvasin  37674  unirep  37684  sdclem2  37712  ssbnd  37758  prdsbnd  37763  cntotbnd  37766  heibor1lem  37779  rrnequiv  37805  ismndo2  37844  grpoeqdivid  37851  isdrngo3  37929  crngohomfo  37976  0idl  37995  1idl  37996  divrngidl  37998  smprngopr  38022  prnc  38037  ispridlc  38040  riotaclbgBAD  38918  lshpdisj  38951  lsateln0  38959  lsatcveq0  38996  opnlen0  39152  cmtbr4N  39219  cvrnbtwn2  39239  cvrnbtwn4  39243  atcvreq0  39278  cvlatexch1  39300  exatleN  39369  atlelt  39403  ps-2  39443  llnn0  39481  lplnn0N  39512  islpln2a  39513  lvoln0N  39556  islvol2aN  39557  4at  39578  dalemcea  39625  dalem3  39629  pmapglb2N  39736  pmapglb2xN  39737  cdlema1N  39756  cdlemb  39759  paddasslem17  39801  llnexchb2lem  39833  llnexchb2  39834  lhpat3  40011  ltrnid  40100  trlne  40150  cdlemc4  40159  cdleme11h  40231  cdlemednuN  40265  cdlemg1a  40535  tendoeq2  40739  tendoid0  40790  dva1dim  40950  dib1dim  41130  dihlatat  41302  dochkrshp4  41354  dochkr1  41443  lclkrlem2e  41476  lcfrlem16  41523  lcfrlem28  41535  mapd0  41630  hdmap14lem13  41845  eqresfnbd  42230  f1o2d2  42231  expeq1d  42320  expeqidd  42321  dvdsexpnn0  42330  reladdrsub  42375  sn-negex12  42406  sn-mullid  42425  sn-mul02  42430  nn0addcom  42440  nn0mulcom  42444  zmulcomlem  42445  mulgt0con1d  42448  mulgt0con2d  42449  sn-sup2  42461  frlmsnic  42510  evlselvlem  42556  prjspner1  42596  elrfi  42664  mrefg2  42677  eldiophb  42727  eldioph2b  42733  diophin  42742  diophun  42743  rexzrexnn0  42774  eldioph4b  42781  diophren  42783  rencldnfilem  42790  pellexlem6  42804  jm2.19  42964  rmydioph  42985  expdiophlem1  42992  expdioph  42994  lnr2i  43087  lpirlnr  43088  hbtlem2  43095  hbtlem4  43097  hbtlem6  43100  dgrsub2  43106  dgraa0p  43120  rngunsnply  43140  nlimsuc  43412  dfsucon  43494  radcnvrat  44286  pm14.24  44404  addrcom  44447  modelaxreplem1  44951  ormklocald  46851  natlocalincr  46853  afveu  47130  dfafn5b  47138  rlimdmafv  47154  afv2eu  47215  rlimdmafv2  47235  el1fzopredsuc  47302  minusmod5ne  47326  elsetpreimafvssdm  47348  imasetpreimafvbijlemfo  47367  sprvalpw  47442  prprvalpw  47477  reupr  47484  fmtnofac2lem  47530  proththdlem  47575  perfectALTVlem2  47684  perfectALTV  47685  gbowpos  47721  gbowgt5  47724  gboge9  47726  nnsum4primesodd  47758  nnsum4primesoddALTV  47759  uhgrimedgi  47851  isuspgrim0  47855  isuspgrimlem  47856  upgrimpths  47870  clnbgrgrim  47895  grimedg  47896  grtrissvtx  47904  stgredgiun  47918  stgrvtx0  47922  isubgr3stgrlem7  47932  grlimgrtrilem2  47955  gpgiedgdmellem  47998  gpgvtxel2  48000  gpgvtx0  48005  gpgvtx1  48006  gpgusgralem  48008  gpgedgvtx0  48013  gpgedgvtx1  48014  gpg3nbgrvtxlem  48017  gpgnbgrvtx0  48024  gpgnbgrvtx1  48025  ringcinvALTV  48233  lincellss  48350  lindsrng01  48392  suppdm  48434  nnpw2pb  48515  0aryfvalel  48562  0aryfvalelfv  48563  itsclc0xyqsolr  48697  infsubc  48975  infsubc2  48976