MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl5bi Structured version   Visualization version   GIF version

Theorem syl5bi 232
Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded antecedent with a definition. (Contributed by NM, 12-Jan-1993.)
Hypotheses
Ref Expression
syl5bi.1 (𝜑𝜓)
syl5bi.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
syl5bi (𝜒 → (𝜑𝜃))

Proof of Theorem syl5bi
StepHypRef Expression
1 syl5bi.1 . . 3 (𝜑𝜓)
21biimpi 206 . 2 (𝜑𝜓)
3 syl5bi.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5 34 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  3imtr4g  285  ancomsd  470  3jao  1387  nfimdOLDOLD  1822  axc16nf  2135  ax13  2247  2euex  2542  2eu1  2551  eqneqall  2802  necon3bd  2805  pm2.61dne  2877  elnelall  2907  spcimgft  3279  rspc  3298  rspcimdv  3305  rspc2gv  3316  euind  3387  reuind  3405  sbciegft  3460  rspsbc  3511  ssexnelpss  3712  ralnralall  4071  pwpw0  4335  sssn  4349  eqsnOLD  4353  prel12  4374  prnebg  4380  pwsnALT  4420  intss1  4483  intmin  4488  uniintsn  4505  iinss  4562  iinss2  4563  disji2  4627  disjiun  4631  disjiund  4634  disjxiun  4640  disjxiunOLD  4641  trel3  4751  trin  4754  trintssOLD  4761  eusvnfb  4853  reusv3  4867  copsexg  4946  propeqop  4960  otiunsndisj  4970  iunopeqop  4971  po3nr  5039  fri  5066  wefrc  5098  wereu2  5101  ssrelrel  5210  relop  5261  iss  5435  restidsingOLD  5447  poirr2  5508  xpcan  5558  xpcan2  5559  sossfld  5568  wfi  5701  wfis2fg  5705  onfr  5751  onmindif  5803  funopg  5910  funssres  5918  funun  5920  fv3  6193  fvmptt  6286  iinpreima  6331  fvn0ssdmfun  6336  dff3  6358  dff4  6359  fmptsng  6419  fmptsnd  6420  tpres  6451  fnprb  6457  fntpb  6458  fvclss  6485  fpropnf1  6509  isomin  6572  isofrlem  6575  weniso  6589  oprabid  6662  ssorduni  6970  onmindif2  6997  limuni3  7037  tfis2f  7040  tfinds  7044  tfinds2  7048  tfinds3  7049  funcnvuni  7104  f1oweALT  7137  f1o2ndf1  7270  poxp  7274  soxp  7275  fnse  7279  suppimacnv  7291  mpt2xopynvov0g  7325  reldmtpos  7345  rntpos  7350  wfrlem14  7413  wfrlem15  7414  onfununi  7423  smoiun  7443  tfrlem1  7457  tfr3  7480  frsucmptn  7519  tz7.49  7525  oaordi  7611  oawordeulem  7619  omeulem1  7647  oeordi  7652  oelimcl  7665  nnaordi  7683  nneob  7717  omsmolem  7718  erdisj  7779  qsss  7793  uniinqs  7812  map0g  7882  resixpfo  7931  ixpsnf1o  7933  xpdom3  8043  mapdom3  8117  phplem4  8127  php3  8131  unxpdomlem3  8151  ssfi  8165  findcard2  8185  findcard3  8188  frfi  8190  isfiniteg  8205  xpfi  8216  fiint  8222  finsschain  8258  dffi2  8314  marypha1lem  8324  marypha2  8330  supmo  8343  suplub2  8352  infmo  8386  ordiso2  8405  ordtypelem7  8414  ordtypelem8  8415  brwdom2  8463  unxpwdom2  8478  ixpiunwdom  8481  elirrv  8489  suc11reg  8501  noinfep  8542  cantnfle  8553  cantnflem1  8571  cantnf  8575  trcl  8589  epfrs  8592  rankpwi  8671  rankunb  8698  rankuni2b  8701  rankxplim3  8729  cplem1  8737  karden  8743  carddom2  8788  fseqenlem2  8833  ac10ct  8842  acni2  8854  acndom  8859  infpwfien  8870  alephordi  8882  alephord  8883  iunfictbso  8922  aceq3lem  8928  dfac5  8936  dfac2  8938  dfac12lem3  8952  dfac12r  8953  cdainflem  8998  cdainf  8999  cfub  9056  cfeq0  9063  coflim  9068  cfslb2n  9075  cofsmo  9076  coftr  9080  infpssr  9115  fin23lem7  9123  fin23lem11  9124  fin23lem21  9146  isf32lem2  9161  isf34lem4  9184  isfin1-2  9192  isfin1-3  9193  fin1a2lem9  9215  fin1a2lem11  9217  fin1a2lem12  9218  fin1a2lem13  9219  domtriomlem  9249  axdc3lem2  9258  axcclem  9264  ac6c4  9288  zorn2lem4  9306  zorn2lem5  9307  zorn2lem7  9309  ttukeylem5  9320  ttukeyg  9324  brdom6disj  9339  fnrndomg  9343  iunfo  9346  iundom2g  9347  ficard  9372  konigthlem  9375  alephval2  9379  pwcfsdom  9390  fpwwe2lem9  9445  fpwwe2lem11  9447  fpwwe2lem12  9448  fpwwe2lem13  9449  pwfseqlem3  9467  gchpwdom  9477  winalim2  9503  gchina  9506  wunex2  9545  tskr1om2  9575  tskxpss  9579  inar1  9582  tskuni  9590  gruun  9613  grudomon  9624  grur1  9627  ltmpi  9711  ltexprlem2  9844  ltexprlem6  9848  reclem2pr  9855  reclem3pr  9856  reclem4pr  9857  suplem1pr  9859  mulgt0sr  9911  supsrlem  9917  axrrecex  9969  axpre-sup  9975  ltlen  10123  addid0  10435  negn0  10444  negf1o  10445  mulge0b  10878  supaddc  10975  supadd  10976  supmul1  10977  supmullem1  10978  supmullem2  10979  supmul  10980  cju  11001  nnsub  11044  0mnnnnn0  11310  un0addcl  11311  un0mulcl  11312  nn0sub  11328  nn0n0n1ge2b  11344  peano5uzi  11451  eluzuzle  11681  zsupss  11762  qbtwnre  12015  xrsupexmnf  12120  xrinfmexpnf  12121  xrsupsslem  12122  xrinfmsslem  12123  xrub  12127  supxrun  12131  ixxdisj  12175  icodisj  12282  difreicc  12289  uzsubsubfz  12348  fzadd2  12361  elfzmlbp  12434  fzofzim  12498  elfznelfzo  12557  injresinj  12572  subfzo0  12573  flval3  12599  modirr  12724  modsumfzodifsn  12726  addmodlteq  12728  ssnn0fi  12767  seqf1o  12825  expcl2lem  12855  expnegz  12877  expaddz  12887  expmulz  12889  facwordi  13059  faclbnd4lem4  13066  bccl  13092  hashnfinnn0  13135  hashgt12el  13193  hashgt12el2  13194  hashfun  13207  hashbclem  13219  hashbc  13220  hashfacen  13221  hashf1lem1  13222  hashf1  13224  hash2pwpr  13241  fundmge2nop0  13257  fi1uzind  13262  brfi1indALT  13265  fi1uzindOLD  13268  brfi1indALTOLD  13271  wrdind  13458  wrd2ind  13459  reuccats1  13462  swrdccatin1  13464  swrdccatin2  13468  swrdccat3  13473  swrdccat3blem  13476  cshw1  13549  cshwcsh2id  13555  wwlktovfo  13682  s3iunsndisj  13688  rtrclreclem3  13781  dfrtrcl2  13783  sqrlem1  13964  sqrlem6  13969  rexanre  14067  cau3lem  14075  2clim  14284  summo  14429  fsum2dlem  14482  fsumiun  14534  prodmo  14647  fprod2dlem  14691  bpolycl  14764  rpnnen2lem12  14935  odd2np1lem  15045  oddge22np1  15054  sqoddm1div8z  15059  sumeven  15091  pwp1fsum  15095  bitsfzo  15138  sadcaddlem  15160  gcd0id  15221  algcvgblem  15271  lcmfunsnlem1  15331  lcmfunsnlem2lem1  15332  lcmfunsnlem2  15334  coprmproddvdslem  15357  divgcdcoprm0  15360  isprm7  15401  prmdvdsexpr  15410  prmfac1  15412  qnumdencl  15428  hashdvds  15461  prm23lt5  15500  pcneg  15559  prmpwdvds  15589  prmreclem2  15602  4sqlem12  15641  vdwlem6  15671  vdwlem10  15675  vdwlem13  15678  0ram  15705  ram0  15707  ramz  15710  ramcl  15714  prmgaplem3  15738  prmgaplem4  15739  prmgaplem5  15740  prmgaplem6  15741  cshwshashlem1  15783  prmlem0  15793  firest  16074  imasaddfnlem  16169  imasvscafn  16178  mremre  16245  cicsym  16445  initoid  16636  termoid  16637  iszeroi  16640  drsdirfi  16919  pospo  16954  joinfval  16982  meetfval  16996  lubun  17104  odupos  17116  acsfiindd  17158  psss  17195  mnd1id  17313  dfgrp2e  17429  dfgrp3lem  17494  symgfix2  17817  f1omvdco2  17849  symggen  17871  odcau  18000  pgpfi  18001  sylow2blem3  18018  sylow3lem2  18024  lsmmod  18069  efgsfo  18133  frgpuptinv  18165  frgpnabllem1  18257  cyggeninv  18266  lt6abl  18277  cyggex2  18279  gsumval3lem2  18288  gsumval3  18289  gsum2d2  18354  dmdprdd  18379  dprd2da  18422  pgpfac1lem5  18459  pgpfac  18464  srgbinomlem4  18524  dvdsrtr  18633  dvdsrmul1  18634  lss1d  18944  lspsolvlem  19123  lspsnat  19126  lbsextlem2  19140  lbsextlem3  19141  0ring  19251  01eq0ring  19253  0ring01eqbi  19254  rng1nfld  19259  domnmuln0  19279  abvn0b  19283  mvrf1  19406  mplcoe5lem  19448  opsrtoslem2  19466  cply1mul  19645  coe1fzgsumdlem  19652  gsummoncoe1  19655  pf1ind  19700  evl1gsumdlem  19701  xrsdsreclblem  19773  qsssubdrg  19786  prmirredlem  19822  cygznlem3  19899  obslbs  20055  dsmmacl  20066  lindfrn  20141  lmiclbs  20157  lmisfree  20162  matecl  20212  mat1dimelbas  20258  scmateALT  20299  mdetdiaglem  20385  mdet0  20393  mdetunilem9  20407  gsummatr01  20446  cpmatmcllem  20504  m2cpminvid2lem  20540  pmatcollpw3fi1lem2  20573  chfacfscmul0  20644  chfacfpmmul0  20648  cayhamlem3  20673  tgcl  20754  tgidm  20765  indistopon  20786  fctop  20789  cctop  20791  ppttop  20792  pptbas  20793  epttop  20794  opnnei  20905  neiptopnei  20917  tgrest  20944  restntr  20967  perfopn  20970  ordtrest2lem  20988  isreg2  21162  lmmo  21165  ordthauslem  21168  cmpsublem  21183  cmpsub  21184  cmpcld  21186  hauscmplem  21190  iunconnlem  21211  unconn  21213  2ndcrest  21238  2ndcctbss  21239  2ndcdisj  21240  dis2ndc  21244  locfincmp  21310  comppfsc  21316  txbas  21351  ptbasin  21361  ptbasfi  21365  txcls  21388  txbasval  21390  ptpjopn  21396  ptclsg  21399  dfac14lem  21401  xkoccn  21403  txcnp  21404  txindis  21418  txdis1cn  21419  tx1stc  21434  tx2ndc  21435  txkgen  21436  xkoco1cn  21441  xkoco2cn  21442  xkococn  21444  xkoinjcn  21471  txconn  21473  fbfinnfr  21626  opnfbas  21627  filtop  21640  isfild  21643  fbunfip  21654  filconn  21668  fbasrn  21669  filuni  21670  isufil2  21693  filssufilg  21696  ufileu  21704  filufint  21705  rnelfmlem  21737  rnelfm  21738  fmfnfmlem2  21740  fmfnfmlem4  21742  fmfnfm  21743  hausflimi  21765  hauspwpwf1  21772  flffbas  21780  flftg  21781  alexsublem  21829  alexsubALTlem1  21832  alexsubALTlem2  21833  alexsubALTlem3  21834  alexsubALTlem4  21835  alexsubALT  21836  ptcmplem3  21839  cldsubg  21895  qustgpopn  21904  tgptsmscld  21935  tsmsxplem1  21937  ustfilxp  21997  imasdsf1olem  22159  bldisj  22184  xbln0  22200  prdsxmslem2  22315  xrsblre  22595  icccmplem2  22607  reconn  22612  opnreen  22615  xrge0tsms  22618  metdsre  22637  iccpnfcnv  22724  cnheiborlem  22734  phtpc01  22777  pi1blem  22820  tchcph  23017  cfilfcls  23053  iscau4  23058  bcthlem5  23106  bcth3  23109  hlhil  23195  ovolctb  23239  ovoliunlem2  23252  ovoliunnul  23256  ovolicc2  23271  volfiniun  23296  iundisj  23297  dyadmax  23347  dyadmbllem  23348  vitalilem2  23359  ismbfd  23388  mbfimaopnlem  23403  itg11  23439  i1faddlem  23441  mbfi1fseqlem4  23466  bddmulibl  23586  limciun  23639  perfdvf  23648  rolle  23734  dvivthlem1  23752  dvne0  23755  lhop1  23758  lhop2  23759  itgsubst  23793  dvdsq1p  23901  fta1g  23908  dgrco  24012  plydivex  24033  fta1  24044  ulmcaulem  24129  abelthlem2  24167  pilem2  24187  cxpmul2z  24418  cxpcn3lem  24469  xrlimcnp  24676  jensen  24696  wilthlem2  24776  wilthlem3  24777  muval2  24841  sqf11  24846  ppiublem1  24908  fsumvma  24919  lgsdir2lem2  25032  lgsdir2lem5  25035  lgsqrmodndvds  25059  gausslemma2dlem1a  25071  gausslemma2dlem3  25074  gausslemma2d  25080  2lgsoddprmlem2  25115  dchrisum0fno1  25181  pntlem3  25279  pntleml  25281  ostthlem1  25297  ostth2lem2  25304  colinearalg  25771  axcontlem2  25826  axcontlem8  25832  edgupgr  26010  umgrpredgv  26016  numedglnl  26020  ausgrumgri  26043  ausgrusgri  26044  ushgredgedg  26102  ushgredgedgloop  26104  uhgr0v0e  26111  subumgredg2  26158  uhgrspansubgrlem  26163  uhgrspan1  26176  upgrreslem  26177  umgrreslem  26178  upgrres1  26186  fusgrfisstep  26202  nbuhgr  26220  nbuhgr2vtx1edgb  26229  uhgrnbgr0nb  26231  edgnbusgreu  26250  nbusgredgeu0  26251  nbusgrf1o0  26252  nbusgrvtxm1uvtx  26287  cusgredg  26301  cusgrfi  26335  usgredgsscusgredg  26336  1loopgrnb0  26379  usgrvd0nedg  26410  uhgrvd00  26411  upgriswlk  26518  upgrwlkcompim  26520  uspgr2wlkeq  26523  uspgr2wlkeqi  26525  wlkv0  26528  wlklenvclwlk  26532  wlkp1lem6  26556  lfgrwlkprop  26565  spthdep  26611  upgrwlkdvdelem  26613  usgr2wlkneq  26633  usgr2trlncl  26637  pthdlem1  26643  pthdlem2lem  26644  clwlkl1loop  26659  crctcshwlkn0lem3  26685  crctcshwlkn0lem5  26687  crctcshwlkn0  26694  0enwwlksnge1  26730  wlkiswwlks2  26742  wlkiswwlksupgr2  26744  wlkwwlksur  26764  umgr2adedgspth  26825  wwlks2onv  26828  clwlkclwwlklem2a4  26879  clwlkclwwlklem2  26882  clwwlksf1  26897  erclwwlkstr  26916  erclwwlksntr  26928  hashecclwwlksn1  26934  umgrhashecclwwlk  26935  clwlksfoclwwlk  26943  eucrctshift  27083  3cyclfrgrrn1  27129  frgrnbnb  27137  frgrncvvdeqlem2  27144  frgrncvvdeqlem3  27145  frgrncvvdeqlem9  27151  frgrwopreglem5  27158  frgrwopreg1  27160  frgrwopreg2  27161  numclwwlkovf2ex  27191  numclwlk1lem2f1  27198  lnon0  27623  shmodsi  28218  shlub  28243  spanunsni  28408  h1datomi  28410  stm1ri  29073  stadd3i  29077  mdsl1i  29150  cvmdi  29153  superpos  29183  chjatom  29186  chirredi  29223  atcvat4i  29226  sumdmdii  29244  sumdmdlem  29247  cdj3lem2a  29265  cdj3lem3a  29268  cdj3i  29270  disji2f  29362  disjif2  29366  iundisjf  29374  rnmpt2ss  29447  iundisjfi  29529  nn0min  29541  xrge0tsmsd  29759  cnre2csqima  29931  ordtrest2NEWlem  29942  xrge0iifcnv  29953  lmxrge0  29972  measdivcstOLD  30261  dya2iocuni  30319  omssubadd  30336  eulerpartlems  30396  bnj849  30969  bnj1118  31026  derangenlem  31127  erdszelem9  31155  pconnconn  31187  iccllysconn  31206  cvmsval  31222  cvmscld  31229  cvmsss2  31230  cvmopnlem  31234  cvmfolem  31235  cvmliftmolem2  31238  cvmlift2lem10  31268  cvmlift2lem12  31270  cvmlift3lem5  31279  cvmlift3lem8  31282  msubvrs  31431  mthmblem  31451  untsucf  31561  3orel1  31566  3orel2  31567  3orel3  31568  nepss  31574  eqfunresadj  31635  dfon2lem5  31666  dfon2lem6  31667  dfon2lem7  31668  dfon2lem8  31669  rdgprc  31674  trpredtr  31704  dftrpred3g  31707  trpredrec  31712  frmin  31713  frind  31714  frins2fg  31718  wzel  31745  wsuclem  31747  wsuclemOLD  31748  frrlem5e  31762  nosepon  31792  noextendseq  31794  nolesgn2ores  31799  nosepdmlem  31807  nodenselem8  31815  noetalem3  31839  nocvxmin  31868  scutun12  31891  funpartfun  32025  altopth1  32047  altopth2  32048  colineardim1  32143  lineext  32158  btwnconn1lem14  32182  brsegle  32190  hilbert1.2  32237  trer  32285  elicc3  32286  finminlem  32287  fneint  32318  fnessref  32327  refssfne  32328  neibastop1  32329  neibastop2lem  32330  neibastop2  32331  fnemeet2  32337  fnejoin2  32339  tailfb  32347  arg-ax  32390  ordtoplem  32409  onsuct0  32415  bj-gl4lem  32554  bj-sngltag  32946  bj-restn0  33018  bj-0int  33030  bj-ismooredr2  33040  bj-bary1lem1  33132  icorempt2  33170  icoreresf  33171  relowlssretop  33182  finxpreclem6  33204  wl-ax8clv2  33352  fin2so  33367  poimirlem24  33404  poimirlem25  33405  poimirlem26  33406  poimirlem27  33407  poimirlem29  33409  poimirlem30  33410  poimirlem31  33411  mblfinlem1  33417  mblfinlem4  33420  ovoliunnfl  33422  itg2addnclem  33432  itg2addnclem2  33433  areacirc  33476  unirep  33478  filbcmb  33506  sdclem1  33510  fdc  33512  nninfnub  33518  isbnd2  33553  ssbnd  33558  prdsbnd2  33565  cntotbnd  33566  heibor1lem  33579  heiborlem1  33581  heiborlem4  33584  heiborlem6  33586  0idl  33795  intidl  33799  unichnidl  33801  keridl  33802  prnc  33837  prtlem17  33980  prter2  33985  ax12indn  34047  lsatn0  34105  lsatcmp  34109  lssat  34122  lfl1  34176  lshpsmreu  34215  lkrin  34270  glbconxN  34483  cvrat4  34548  paddasslem17  34941  pmodlem2  34952  dalawlem14  34989  pclclN  34996  pclfinN  35005  pclfinclN  35055  poml4N  35058  osumcllem8N  35068  pexmidlem5N  35079  cdleme32a  35548  cdlemg33b0  35808  tendoeq2  35881  diaelrnN  36153  dihmeetlem1N  36398  dihglblem5apreN  36399  dihglblem2N  36402  dochvalr  36465  dochkrshp  36494  lcfl6  36608  lcfrvalsnN  36649  mapdordlem2  36745  mapdh8b  36888  mapdh9a  36898  hdmap14lem13  36991  eldioph2b  37145  eldiophss  37157  diophren  37196  ctbnfien  37201  rencldnfilem  37203  pellexlem3  37214  pellexlem5  37216  pellex  37218  pell14qrexpcl  37250  pellfundre  37264  pellfundge  37265  pellfundlb  37267  pellfundglb  37268  jm2.19lem4  37378  fnwe2lem2  37440  pwssplit4  37478  hbtlem5  37517  ss2iundf  37770  relexpmulg  37821  relexpxpmin  37828  relexpaddss  37829  dftrcl3  37831  dfrtrcl3  37844  clsk1indlem3  38161  isotone1  38166  isotone2  38167  ntrneiel2  38204  ntrneik4w  38218  onfrALT  38584  ax6e2ndeq  38595  snssiALT  38883  iinssf  39147  hirstL-ax3  40822  2reurex  40944  otiunsndisjX  41061  subsubelfzo0  41099  iccpartiltu  41122  iccpartigtl  41123  iccpartltu  41125  pfxccat3  41191  pfxccat3a  41194  reuccatpfxs1  41199  fmtnofac2lem  41245  fmtno4prmfac  41249  prmdvdsfmtnof1lem1  41261  lighneallem2  41288  opoeALTV  41359  opeoALTV  41360  even3prm2  41393  gbegt5  41414  gbowgt5  41415  sbgoldbwt  41430  sbgoldbst  41431  sbgoldbalt  41434  sbgoldbm  41437  mogoldbb  41438  sbgoldbo  41440  nnsum3primesle9  41447  nnsum4primeseven  41453  nnsum4primesevenALTV  41454  wtgoldbnnsum4prm  41455  bgoldbnnsum3prm  41457  bgoldbtbndlem1  41458  bgoldbtbndlem4  41461  bgoldbtbnd  41462  upgrwlkupwlk  41486  sprsymrelf1lem  41506  sprsymrelfolem2  41508  sprsymrelf1  41511  sprsymrelfo  41512  mgmpropd  41540  copisnmnd  41574  mgm2mgm  41628  ringrng  41644  c0snmgmhm  41679  ztprmneprm  41890  mndpsuppss  41917  lindslinindimp2lem4  42015  lindslinindsimp2  42017  lindsrng01  42022  snlindsntor  42025  ldepspr  42027  isldepslvec2  42039  suppdm  42065  blen1b  42147  dignn0ldlem  42161  digexp  42166  nn0sumshdiglemB  42179  nn0sumshdiglem1  42180  iunord  42187  tfis2d  42192
  Copyright terms: Public domain W3C validator