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  4538  elsn2g  4664  preq1b  4846  elpreqprb  4868  reusv3  5405  alxfr  5407  reuhypd  5419  axpr  5427  opth1  5480  euotd  5518  otiunsndisj  5525  tz7.2  5668  frsn  5773  dmopab2rex  5928  elsnxp  6311  reuop  6313  dfpo2  6316  ordtri1  6417  ordtri3  6420  fvmptdv2  7034  fveqressseq  7099  foco2  7129  fsn  7155  fnsnb  7186  fmptsng  7188  fmptsnd  7189  fconst2g  7223  fnprb  7228  fntpb  7229  funfvima  7250  soisoi  7348  isores3  7355  eqfunresadj  7380  riotaeqimp  7414  eusvobj2  7423  ovmpodv2  7591  f1opw2  7688  sorpssun  7750  sorpssin  7751  oneqmin  7820  nlimsucg  7863  onzsl  7867  tfinds  7881  funcnvuni  7954  mptcnfimad  8011  opiota  8084  mposn  8128  frpoins3xpg  8165  frpoins3xp3g  8166  poxp2  8168  xpord2pred  8170  sexp2  8171  poxp3  8175  xpord3pred  8177  sexp3  8178  xpord3inddlem  8179  suppssov1  8222  suppssov2  8223  suppssfv  8227  brtpos  8260  frrlem12  8322  frrlem13  8323  wfrlem10OLD  8358  wfrlem14OLD  8362  wfrlem15OLD  8363  seqomlem1  8490  seqomlem2  8491  omordi  8604  omord  8606  omwordi  8609  oeeui  8640  nnmordi  8669  nnmord  8670  nnmwordi  8673  nnawordex  8675  nnaordex  8676  nneob  8694  omsmolem  8695  eldifsucnn  8702  qsss  8818  eroveu  8852  mapsncnv  8933  ralxpmap  8936  elixpsn  8977  ixpsnf1o  8978  boxcutc  8981  pw2f1olem  9116  2pwne  9173  mapxpen  9183  mapunen  9186  php  9247  phpOLD  9259  onomeneq  9265  unxpdomlem2  9287  en1eqsnbi  9310  isfiniteg  9337  fofinf1o  9372  f1opwfi  9396  elfiun  9470  oieu  9579  brwdom2  9613  wdomtr  9615  ixpiunwdom  9630  en3lplem1  9652  suc11reg  9659  inf3lemd  9667  cantnfvalf  9705  cantnflt  9712  cantnfp1lem3  9720  cantnflem2  9730  ttrcltr  9756  rnttrcl  9762  ttrclselem1  9765  r1tr  9816  updjud  9974  dfac8alem  10069  wdomnumr  10104  isinfcard  10132  aceq3lem  10160  dfac5lem4  10166  dfac5lem4OLD  10168  dfac5  10169  dfac2b  10171  coftr  10313  fin23lem28  10380  fin23lem29  10381  fin1a2lem11  10450  fin1a2lem12  10451  fin1a2lem13  10452  hsmexlem9  10465  axdclem  10559  pwcfsdom  10623  gchdomtri  10669  fpwwe2  10683  gchpwdom  10710  gchhar  10719  addnidpi  10941  nqereu  10969  genpv  11039  genpdm  11042  distrlem5pr  11067  mulrid  11259  ltne  11358  mul02  11439  cnegex  11442  mul0or  11903  negfi  12217  sup2  12224  supaddc  12235  supadd  12236  supmul1  12237  supmul  12240  creur  12260  creui  12261  cju  12262  nnsub  12310  un0addcl  12559  un0mulcl  12560  nn0sub  12576  elz2  12631  zaddcl  12657  suprzcl2  12980  qmulz  12993  qre  12995  qnegcl  13008  elpqb  13018  xrmax1  13217  xrmin2  13220  max1ALT  13228  xlesubadd  13305  xmulass  13329  xlemul1a  13330  xrsupexmnf  13347  xrinfmexpnf  13348  xrub  13354  iccid  13432  fzsn  13606  fzsuc2  13622  fz1sbc  13640  elfzp12  13643  modmuladd  13954  seqid3  14087  bcval5  14357  bcpasc  14360  hashbnd  14375  hashnnn0genn0  14382  hashprg  14434  hashfzo  14468  tpfo  14539  wrdl1s1  14652  ccats1alpha  14657  cats1un  14759  s7f1o  15005  shftlem  15107  replim  15155  absmod0  15342  absz  15350  rlimdm  15587  summolem2  15752  summo  15753  zsum  15754  fsum  15756  fsummulc2  15820  fsumconst  15826  fsum00  15834  incexclem  15872  isumsplit  15876  infcvgaux1i  15893  prodmolem2  15971  prodmo  15972  zprod  15973  fprod  15977  prodsn  15998  prodsnf  16000  fprodconst  16014  ruclem2  16268  fzo0dvdseq  16360  bitsf1ocnv  16481  sadcaddlem  16494  smueqlem  16527  gcdabs1  16566  bezoutlem1  16576  bezoutlem3  16578  bezoutlem4  16579  dvdsgcd  16581  dvdsmulgcd  16593  lcmgcdeq  16649  lcmf  16670  lcmfunsnlem1  16674  lcmfunsnlem2lem2  16676  isprm2lem  16718  dvdsprime  16724  isprm5  16744  coprm  16748  prmdvdsexpr  16754  rpexp  16759  phibndlem  16807  dfphi2  16811  hashgcdlem  16825  odzdvds  16833  nnoddn2prm  16849  pythagtriplem1  16854  iserodd  16873  pceulem  16883  pcqmul  16891  pcqcl  16894  pcxnn0cl  16898  pcxcl  16899  pcneg  16912  pcabs  16913  pcgcd1  16915  pcz  16919  pcprmpw2  16920  pcprmpw  16921  dvdsprmpweqle  16924  difsqpwdvds  16925  pcaddlem  16926  pcadd  16927  pcmpt  16930  pockthg  16944  prmreclem5  16958  4sqlem4  16990  mul4sq  16992  vdwapun  17012  vdwlem2  17020  vdwlem6  17024  vdwlem8  17026  vdwlem13  17031  0ram  17058  ram0  17060  ramcl  17067  cshwsiun  17137  wunress  17295  wunressOLD  17296  firest  17477  isssc  17864  pospo  18390  latnlej  18501  gsumval2a  18698  xpsmnd0  18791  mnd1id  18793  0subm  18830  mulgnn0p1  19103  mulgnn0ass  19128  cyccom  19221  gicsubgen  19297  symg1bas  19408  snsymgefmndeq  19412  psgnunilem1  19511  psgnunilem2  19513  mndodcongi  19561  oddvdsnn0  19562  odnncl  19563  oddvds  19565  odeq  19568  odeq1  19578  pgpfi2  19624  sylow2a  19637  sylow2blem3  19640  sylow3lem6  19650  lsmelvalm  19669  lsmsubm  19671  lsmsubg  19672  lsmmod  19693  lsmdisj2  19700  efgmnvl  19732  efgtlen  19744  efgs1b  19754  efgrelexlemb  19768  efgredeu  19770  efgcpbllemb  19773  frgpuptinv  19789  frgpup3lem  19795  qusabl  19883  frgpnabllem1  19891  cyggeninv  19901  cyggenod  19902  gsumval3eu  19922  dprdssv  20036  dprdfeq0  20042  dprdsubg  20044  dprddisj2  20059  ablfacrp  20086  pgpfac1lem3  20097  pgpfaclem2  20102  xpsring1d  20330  dvreq1  20411  irredn1  20426  nzrunit  20524  ringcinv  20671  rrgeq0  20700  domneq0  20708  drngmul0orOLD  20761  isabvd  20813  abvdom  20831  issrngd  20856  lmodfopnelem2  20897  lss1d  20961  lspsneq0  21010  lbspss  21081  lsmcl  21082  lvecvs0or  21110  lspindpi  21134  lidl1el  21236  lpiss  21339  lidldvgen  21344  qsssubdrg  21444  zringlpirlem1  21473  pzriprnglem6  21497  pzriprnglem12  21503  znfld  21579  znunit  21582  znrrg  21584  cygznlem3  21588  frgpcyg  21592  psgnghm  21598  ipeq0  21656  cssincl  21706  lsmcss  21710  obselocv  21748  dsmmacl  21761  dsmmlss  21764  mplsubrglem  22024  mplmonmul  22054  mplcoe5lem  22057  mhpsclcl  22151  mhpvarcl  22152  psdmul  22170  coe1tmmul2  22279  coe1tmmul  22280  pf1ind  22359  mat1dimelbas  22477  mdetralt  22614  mdetunilem2  22619  mdetunilem7  22624  mdetunilem9  22626  maducoeval2  22646  chpscmat  22848  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  istopon  22918  eltg3  22969  tgidm  22987  clsval2  23058  opncldf1  23092  restbas  23166  tgrest  23167  restcld  23180  restcldr  23182  restcls  23189  restntr  23190  ordtbas2  23199  ordtbas  23200  ordtrest2lem  23211  ordtrest2  23212  pnfnei  23228  mnfnei  23229  tgcn  23260  cnconst  23292  cnindis  23300  lmss  23306  ordtt1  23387  discmp  23406  1stcrest  23461  2ndcdisj  23464  cldllycmp  23503  txbas  23575  ptpjpre1  23579  ptuni2  23584  ptbasin  23585  ptbasfi  23589  ptopn2  23592  txbasval  23614  ptpjopn  23620  ptclsg  23623  dfac14lem  23625  xkoccn  23627  ptcnp  23630  upxp  23631  ptrescn  23647  txkgen  23660  xkoptsub  23662  xkopt  23663  xkoco1cn  23665  xkoco2cn  23666  xkococn  23668  xkoinjcn  23695  ordthmeolem  23809  ptuncnv  23815  nrmhaus  23834  fbssint  23846  fbfinnfr  23849  fbasrn  23892  isufil2  23916  filufint  23928  rnelfm  23961  fmfnfmlem2  23963  fmfnfmlem3  23964  fmfnfmlem4  23965  fmfnfm  23966  flimtopon  23978  flimclslem  23992  fclstopon  24020  fclscf  24033  flimfnfcls  24036  alexsublem  24052  alexsubALTlem3  24057  alexsubALTlem4  24058  ptcmplem2  24061  tmdgsum2  24104  symgtgp  24114  cldsubg  24119  qustgplem  24129  tgptsmscld  24159  tsmsxplem1  24161  imasdsf1olem  24383  blssps  24434  blss  24435  stdbdxmet  24528  methaus  24533  metrest  24537  nrginvrcn  24713  nmoeq0  24757  blssioo  24816  xrtgioo  24828  xrsxmet  24831  reconnlem1  24848  reconnlem2  24849  xrge0tsms  24856  elcncf1di  24921  iccpnfcnv  24975  evth  24991  lebnumlem1  24993  lebnumlem2  24994  lebnumlem3  24995  nmoleub3  25152  minveclem3b  25462  ivthlem2  25487  ivthlem3  25488  elovolm  25510  ovolmge0  25512  ovoliun  25540  ovolicc2lem3  25554  ovolicc2  25557  voliunlem3  25587  dyaddisj  25631  dyadmax  25633  opnmblALT  25638  ismbfd  25674  ismbf2d  25675  mbfimaopnlem  25690  mbfimaopn2  25692  i1fmullem  25729  i1fres  25740  itg1climres  25749  mbfi1fseqlem4  25753  itg2lcl  25762  itgsplitioo  25873  ellimc2  25912  rolle  26028  dvlip  26032  dvge0  26045  dvne0  26050  lhop1lem  26052  tdeglem4  26099  degltlem1  26111  deg1nn0clb  26129  deg1lt0  26130  dvdsq1p  26202  ply1rem  26205  fta1g  26209  elply2  26235  plyf  26237  ne0p  26246  plyeq0lem  26249  plypf1  26251  0dgrb  26285  coe1termlem  26297  dgrcolem2  26314  plymul0or  26322  plyrem  26347  fta1  26350  quotcan  26351  aalioulem3  26376  eff1olem  26590  lognegb  26632  eflogeq  26644  argregt0  26652  argrege0  26653  tanarg  26661  cxpexp  26710  cxpeq0  26720  mulcxp  26727  cxpeq  26800  atans2  26974  scvxcvx  27029  dmgmaddn0  27066  isppw2  27158  vmappw  27159  vmacl  27161  efvmacl  27163  isnsqf  27178  mumullem2  27223  sqff1o  27225  dvdsppwf1o  27229  ppiublem1  27246  vmalelog  27249  chtublem  27255  fsumvma  27257  perfectlem2  27274  perfect  27275  bposlem1  27328  lgsmod  27367  lgsne0  27379  lgsdirnn0  27388  lgsqr  27395  lgsdchr  27399  gausslemma2dlem1a  27409  gausslemma2dlem6  27416  lgseisenlem2  27420  lgsquadlem1  27424  lgsquadlem2  27425  2lgslem1b  27436  2sqlem2  27462  mul2sq  27463  2sqlem7  27468  dchrisum0fno1  27555  pntrsumbnd2  27611  ostthlem1  27671  ostth2lem2  27678  ostth3  27682  ostth  27683  nolesgn2ores  27717  nogesgn1ores  27719  nolt02o  27740  nogt01o  27741  nosupbnd2  27761  noinfbnd2lem1  27775  noetasuplem4  27781  noetainflem4  27785  maxs1  27810  mins2  27813  sltne  27815  ssltsn  27837  cuteq1  27878  madef  27895  sltlpss  27945  lrrecfr  27976  addsval  27995  addsproplem2  28003  addsuniflem  28034  addsbdaylem  28049  negsid  28073  negsunif  28087  mulsproplem5  28146  mulsproplem6  28147  mulsproplem7  28148  mulsproplem8  28149  mulsproplem9  28150  slemuld  28164  ssltmul1  28173  ssltmul2  28174  sltmul2  28197  muls0ord  28211  precsexlem8  28238  precsexlem9  28239  precsexlem11  28241  elons2  28281  onaddscl  28286  onmulscl  28287  nnsge1  28346  n0subs  28360  dfnns2  28362  znegscl  28378  zaddscl  28380  zmulscld  28383  elzn0s  28384  eln0zs  28386  n0seo  28405  zseo  28406  zs12bday  28424  recut  28428  0reno  28429  remulscllem1  28432  colinearalg  28925  axpasch  28956  axlowdimlem16  28972  axlowdimlem17  28973  axlowdim  28976  axcontlem2  28980  axcontlem4  28982  axcontlem7  28985  lpvtx  29085  edglnl  29160  numedglnl  29161  usgredgop  29187  usgrexmplef  29276  uhgrspansubgrlem  29307  uhgrspan1  29320  nbusgredgeu0  29385  nb3grprlem2  29398  cusgrsize2inds  29471  vtxd0nedgb  29506  rusgrpropnb  29601  upgrwlkvtxedg  29663  wlkp1lem1  29691  wlkp1lem6  29696  wlkp1lem8  29698  usgr2wlkneq  29776  crctcshwlk  29842  crctcsh  29844  iswwlksnon  29873  wlkiswwlks1  29887  wwlksnextbi  29914  wwlksnextproplem2  29930  wspthsnonn0vne  29937  clwlkclwwlklem2  30019  clwwisshclwws  30034  erclwwlktr  30041  clwwlkel  30065  clwwlkext2edg  30075  erclwwlkntr  30090  clwlknf1oclwwlknlem2  30101  clwlknf1oclwwlknlem3  30102  clwlknf1oclwwlkn  30103  clwwlknonccat  30115  0wlkons1  30140  3wlkdlem6  30184  eupth2eucrct  30236  frgrwopreglem2  30332  2clwwlk2clwwlk  30369  wlkl0  30386  nvmul0or  30669  ipasslem5  30854  ipasslem11  30859  hvmul0or  31044  his6  31118  hhssnv  31283  ocsh  31302  ocin  31315  shsidmi  31403  chnlen0  31463  h1de2bi  31573  h1de2ctlem  31574  h1de2ci  31575  spansni  31576  3oalem1  31681  nmcexi  32045  atcveq0  32367  chcv1  32374  cdjreui  32451  cdj3lem2b  32456  xrge0tsmsd  33065  1fldgenq  33324  ccfldextdgrr  33722  ordtrest2NEWlem  33921  ordtrest2NEW  33922  xrge0iifcnv  33932  esumc  34052  esumpcvgval  34079  ballotlemfc0  34495  ballotlemfcc  34496  gblacfnacd  35113  subfacp1lem4  35188  subfacp1lem5  35189  erdszelem8  35203  sconnpi1  35244  cvmsss2  35279  cvmlift2lem12  35319  satfv0  35363  satfv0fun  35376  satf00  35379  sat1el2xp  35384  fmla0xp  35388  fmlasucdisj  35404  satffunlem1lem1  35407  satffunlem2lem1  35409  dmopab3rexdif  35410  msubco  35536  msubvrs  35565  ellcsrspsn  35646  sinccvglem  35677  untsucf  35710  nnuni  35727  dfrdg2  35796  colineardim1  36062  btwnconn1lem14  36101  segleantisym  36116  colinbtwnle  36119  outsidele  36133  lineunray  36148  linethru  36154  elicc3  36318  opnregcld  36331  cldregopn  36332  fnejoin2  36370  bj-isrvec  37295  dissneqlem  37341  icorempo  37352  relowlssretop  37364  relowlpssretop  37365  rdgssun  37379  finxpsuclem  37398  lindsenlbs  37622  ptrecube  37627  poimirlem6  37633  poimirlem7  37634  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem23  37650  poimirlem24  37651  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  poimirlem29  37656  poimirlem30  37657  poimirlem31  37658  poimirlem32  37659  itg2addnclem3  37680  ftc1anclem6  37705  dvasin  37711  unirep  37721  sdclem2  37749  ssbnd  37795  prdsbnd  37800  cntotbnd  37803  heibor1lem  37816  rrnequiv  37842  ismndo2  37881  grpoeqdivid  37888  isdrngo3  37966  crngohomfo  38013  0idl  38032  1idl  38033  divrngidl  38035  smprngopr  38059  prnc  38074  ispridlc  38077  riotaclbgBAD  38955  lshpdisj  38988  lsateln0  38996  lsatcveq0  39033  opnlen0  39189  cmtbr4N  39256  cvrnbtwn2  39276  cvrnbtwn4  39280  atcvreq0  39315  cvlatexch1  39337  exatleN  39406  atlelt  39440  ps-2  39480  llnn0  39518  lplnn0N  39549  islpln2a  39550  lvoln0N  39593  islvol2aN  39594  4at  39615  dalemcea  39662  dalem3  39666  pmapglb2N  39773  pmapglb2xN  39774  cdlema1N  39793  cdlemb  39796  paddasslem17  39838  llnexchb2lem  39870  llnexchb2  39871  lhpat3  40048  ltrnid  40137  trlne  40187  cdlemc4  40196  cdleme11h  40268  cdlemednuN  40302  cdlemg1a  40572  tendoeq2  40776  tendoid0  40827  dva1dim  40987  dib1dim  41167  dihlatat  41339  dochkrshp4  41391  dochkr1  41480  lclkrlem2e  41513  lcfrlem16  41560  lcfrlem28  41572  mapd0  41667  hdmap14lem13  41882  fnsnbt  42271  eqresfnbd  42273  f1o2d2  42274  expeq1d  42359  expeqidd  42360  dvdsexpnn0  42369  reladdrsub  42415  sn-negex12  42446  sn-mullid  42465  sn-mul02  42470  nn0addcom  42480  nn0mulcom  42484  zmulcomlem  42485  mulgt0con1d  42488  mulgt0con2d  42489  sn-sup2  42501  frlmsnic  42550  evlselvlem  42596  prjspner1  42636  elrfi  42705  mrefg2  42718  eldiophb  42768  eldioph2b  42774  diophin  42783  diophun  42784  rexzrexnn0  42815  eldioph4b  42822  diophren  42824  rencldnfilem  42831  pellexlem6  42845  jm2.19  43005  rmydioph  43026  expdiophlem1  43033  expdioph  43035  lnr2i  43128  lpirlnr  43129  hbtlem2  43136  hbtlem4  43138  hbtlem6  43141  dgrsub2  43147  dgraa0p  43161  rngunsnply  43181  nlimsuc  43454  dfsucon  43536  radcnvrat  44333  pm14.24  44451  addrcom  44494  modelaxreplem1  44995  ormklocald  46889  natlocalincr  46891  afveu  47165  dfafn5b  47173  rlimdmafv  47189  afv2eu  47250  rlimdmafv2  47270  el1fzopredsuc  47337  minusmod5ne  47351  elsetpreimafvssdm  47373  imasetpreimafvbijlemfo  47392  sprvalpw  47467  prprvalpw  47502  reupr  47509  fmtnofac2lem  47555  proththdlem  47600  perfectALTVlem2  47709  perfectALTV  47710  gbowpos  47746  gbowgt5  47749  gboge9  47751  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  isuspgrim0  47872  isuspgrimlem  47874  clnbgrgrim  47902  grimedg  47903  grtrissvtx  47911  stgredgiun  47925  stgrvtx0  47929  isubgr3stgrlem7  47939  grlimgrtrilem2  47962  gpgvtxel2  48006  gpgedgel  48007  gpgvtx0  48008  gpgvtx1  48009  gpgusgralem  48011  gpgedgvtx0  48019  gpgedgvtx1  48020  gpg3nbgrvtxlem  48023  gpgnbgrvtx0  48030  gpgnbgrvtx1  48031  ringcinvALTV  48226  lincellss  48343  lindsrng01  48385  suppdm  48427  nnpw2pb  48508  0aryfvalel  48555  0aryfvalelfv  48556  itsclc0xyqsolr  48690